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

[Dan Liew]

Hi,

On 10 May 2017 at 03:55, 曾杰 <zyj183247166 at 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