WIP: Reimplementation of symbolic heap

tracer-x / TracerX

TracerX Symbolic Virtual Machine

https://tracer-x.github.io/

Other

31 stars 11 forks source link

WIP: Reimplementation of symbolic heap #281

Closed domainexpert closed 7 years ago

domainexpert commented 7 years ago

For resolving issue #278 . Not ready to be merged yet.

domainexpert commented 7 years ago

At the moment the run for basic/pointer_struct1.c of klee-examples repository no longer hides the error, but the run for basic/malloc3.c has no subsumption(s). For this, we need to properly record the historical state in the interpolant and use address translation at subsumption checks.

domainexpert commented 7 years ago

@rasoolmaghareh I close this PR now since it seems I am no able to add more commits to it, possibly due to our tracer-x/klee recently gets unforked from klee/klee (see klee/klee#188), causing nasty things happening in the background. I will submit another PR as a continuation of this one.

rasoolmaghareh commented 7 years ago

noted. :+1: