Conversation
michael-schwarz
left a comment
There was a problem hiding this comment.
I added a few minor comments here and there, but overall I think this is a great step in the right direction. It looks like our various HoareDomains now have a sound footing in theory, so they'll hopefully cause no more issues (or if they do, it is much better understood than what we currently had)
|
Does this PR also attempt to fix tests 02/{91, 92, 92} that are also closely related to the address domain? |
Not at all. On the contrary, it makes the problem even worse since previously |
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
I just added the tests for these easier cases as well, which aren't listed in #822. Turns out that the first field one actually accidentally still works due to some of those special cases in lval domain still being present (and thus considering the two buckets, which are represented by themselves, equal). It doesn't work for the zero index since there the index gets turned into top for the bucket representative. |
CHANGES: Functionally equivalent to Goblint in SV-COMP 2023. * Add automatic configuration tuning (goblint/analyzer#772). * Add many library function specifications (goblint/analyzer#865, goblint/analyzer#868, goblint/analyzer#878, goblint/analyzer#884, goblint/analyzer#886). * Reorganize library stubs (goblint/analyzer#814, goblint/analyzer#845). * Add Trace Event Format output to timing (goblint/analyzer#844). * Optimize domains for address and path sets (goblint/analyzer#803, goblint/analyzer#809).
Related to issues #101 and #803.
TODO
SetDomain.Joinedis used insideAddressDomain?HoareDomain.MapBotfor witness generation?SensitiveDomaintoBucketSetDomainor something?