PrivPrecCompare: Add bot_in_blob_leq_bot so bot and Blob(bot) are considered equal#1645
PrivPrecCompare: Add bot_in_blob_leq_bot so bot and Blob(bot) are considered equal#1645michael-schwarz merged 2 commits intomasterfrom
bot_in_blob_leq_bot so bot and Blob(bot) are considered equal#1645Conversation
|
I haven't thought about it much or checked if this would completely break something, but I wonder if such thing could/should be non-optional. I think I suspect domain quickchecking doesn't really work on |
|
I am also not sure if one wants to have this in general, but I think having it in the compare scripts and having the option to dis/enable it, seems like it is generally a step in the right direction? |
|
Do we want to merge this or close it? I'm fine with either! |
|
I was wondering about these analyzer/src/cdomain/value/cdomains/valueDomain.ml Lines 603 to 604 in 99df9da But they're actually after these: analyzer/src/cdomain/value/cdomains/valueDomain.ml Lines 589 to 590 in 99df9da So the special cases don't even trigger for such things. Indeed, then this isn't what should normally happen, but I'm ok with having it for comparison. |
This was needed to not report spurious precision differences for the benchmarks in my thesis.
If we want this on the main branch, we can merge, otherwise we can close it.