search

diffblue / 2ls

Static Analyzer and Verifier
http://www.cprover.org/2LS
Other
43 stars 22 forks source link

Multiple fixes for SV-COMP #134

Closed viktormalik closed 5 years ago

viktormalik commented 5 years ago

Difference rows for different instances of the same dynamic object (same allocation site) are forbidden, since two such objects cannot exist simultaneously in a single iteration.

viktormalik commented 5 years ago

This is needed for SV-COMP, there is 1 false negative in ReachSafety-Heap otherwise.

viktormalik commented 5 years ago

The last 2 commits should resolve the problem with invalid witnesses for memleaks (valid-memtrack).

viktormalik commented 5 years ago

Should I also increment the version number to 0.7.1?

peterschrammel commented 5 years ago

0.7.2

peterschrammel commented 5 years ago

@viktormalik, needs rebasing. Can be merged then.

viktormalik commented 5 years ago

@peterschrammel rebased.