Improve checking when a symbolic deref can be reused.

diffblue / 2ls

Static Analyzer and Verifier

http://www.cprover.org/2LS

Other

43 stars 22 forks source link

Improve checking when a symbolic deref can be reused. #129

Closed viktormalik closed 5 years ago

viktormalik commented 5 years ago

Do not reuse a symbolic dereference in case some aliasing object (or a field of an object) has been assigned after the last definition of the symbolic dereference. Resolves the problem in #128.

viktormalik commented 5 years ago

Fixed bug in detection of dynamic memory usage in loops. This removes numerous false positives in ReachSafety-Heap in SV-COMP.