analyzer
analyzer copied to clipboard
Re-consider `exp.volatiles_are_top` as default
We currently enable this everywhere, which leads to volatile and extern variables always having the value T.
While this of course safe and makes sense when analyzing e.g. drivers, it may be unnecessarily imprecise to consider all volatiles T in other settings. We should, e.g., investigate if this can be turned off for sv-comp at least.
It would also be worth checking if sv-benchmarks even use these. There shouldn't be any externs since the programs are supposed to be closed. There might be volatiles though.
The other thing to review is how well exp.volatiles_are_top is followed at all. AFAIK Apron analysis doesn't even consider that, but if we have such an option, then the support should be consistent.
There are a few places in sv-comp where volatiles are used, though it does not seem like there are sufficient numbers to justify doing this for this year's svcomp.