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!_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
