Thanks a lot!
------------------ ???????? ------------------
??????: "Dan Liew"<d...@su-root.co.uk>;
????????: 2017??5??11??(??????) ????7:53
??????: "????"<zyj183247...@qq.com>;
????: "klee-dev"<klee-dev@imperial.ac.uk>;
????: Re: [klee-dev] One phenomenon after the execution using klee
Hi,
On 10 May 2017 at 03:55, ???? <zyj183247...@qq.com> 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
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
