Hi, On 10 May 2017 at 03:55, 曾杰 <[email protected]> wrote: > 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.
This sounds like a bug but I find your description difficult to read. Could please open an issue on our issue tracker [1] with precise reproduction steps (i.e. the commands and source files to reproduce the issue). [1] https://github.com/klee/klee/issues _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
