[klee-dev] 回复： One phenomenon after the execution using klee

[曾杰]

Thanks a lot!




------------------ 原始邮件 ------------------
发件人: "Dan Liew"<dan at su-root.co.uk>; 
发送时间: 2017年5月11日(星期四) 晚上7:53
收件人: "曾杰"<zyj183247166 at qq.com>; 
抄送: "klee-dev"<klee-dev at imperial.ac.uk>; 
主题: Re: [klee-dev] One phenomenon after the execution using klee



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
-------------- next part --------------
HTML attachment scrubbed and removed