[klee-dev] One phenomenon after the execution using klee

[曾杰]

Hi, all,     If you write test.c with an error out of bound and test2.c with an error assertion failed.
     You first symbolically execution test.bc(using clang to generate), and then the test2.c. you will find the contents in klee-last are different from the latest generated contents in klee-out-n.
     klee-last will have an xxx.assert.err and an xxx.ptr.err both. But the latest generate contents in klee-out-n which is because of the symbolic execution of test2.bc only have the xxx.assertion.err.
     It is just one phenomenon which disobey the rule that klee-last points to the latest directory klee-out-n and not an error. I just present it.


     Best wishes for you!
-------------- next part --------------
HTML attachment scrubbed and removed