Re-consider exp.volatiles_are_top

[michael-schwarz]

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.

[sim642]

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.

[michael-schwarz]

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.

[sim642]

As noted in #1552 (comment), only the none base privatization even considers the option (for locals). And for some reason during writing, not reading.

So there's a lot to reconsider here besides just the default. Other privatizations and other (relational) value analyses don't use this option and thus behave differently. The option probably makes sense for embedded/driver code, at least for volatile globals, but all value analyses should then actually respect it, otherwise they will still return more precise values.