This implements fixes for problems mostly created during the recent CBMC rebase that were revealed in SV-COMP runs.
These are in particular:
Fix of dynobj_instance_analysis which caused that dynamic objects were never split into multiple instances. This, however, broke heap regression tests.
Fix usage of allocation guards w.r.t. new malloc implementation in CBMC that makes the regression tests work again.
Fix collection of record::free vars w.r.t. new free implementation.
Drop conditional update of dynamic objects which caused some false positive results (due to over-approximation) and which shouldn't be necessary since we use dynamic object instances (that should guarantee soundness).
Improve resolution of pointed-to objects obtained from the solver in heap domain.
Workaround for an SSA creation bug that occurs when a single SKIP instruction is a target of both a forward and a backward GOTO.
... and some more (see individual commits)
Besides that, CBMC prerequisite is updated to the newest version (may require rebase once peterschrammel/cbmc#27 is merged).
This implements fixes for problems mostly created during the recent CBMC rebase that were revealed in SV-COMP runs.
These are in particular:
dynobj_instance_analysis
which caused that dynamic objects were never split into multiple instances. This, however, broke heap regression tests.malloc
implementation in CBMC that makes the regression tests work again.record::free
vars w.r.t. newfree
implementation.Besides that, CBMC prerequisite is updated to the newest version (may require rebase once peterschrammel/cbmc#27 is merged).