[klee-dev] klee can't handle when the constant is a statement label, how to solve this problem?

[Xuzhijian]

Hi,all,I'm sorry to disturb you.
I had open an issue on GitHub(https://github.com/klee/klee/issues/615), Klee 
can't handle the constant when it is a statement label. I gave a test example 
before and thanks andreamattavelli gave me 
a solution. However, this solution can't solve this problem perfectly. I make a 
little change to the testcase:

#include 
#include 

unsigned long test_func(int x)
{
unsigned long ret;
if ( x == 'p' )
{
printf("addr_flag=%lx\n", (unsigned long)&_flag);
ret = (unsigned long)&_flag;
return ret;
}

ret = x;
addr_flag:
return ret;
}
int main()
{
int a;
klee_make_symbolic(, sizeof(a), "a");
return !!test_func(a);
}

Klee gives the same error again.

# klee -optimize test.bc
KLEE: output directory is "/home/odysseus/tmp/klee-out-2"
Using STP solver backend
KLEE: WARNING: undefined reference to function: printf
LLVM ERROR: invalid argument to evalConstant()

How to solve this problem? Hope for your help! Thank you very much.

Zhijian Xu
5/11/2017
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

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

[????]

Thanks a lot!




--  --
??: "Dan Liew"; 
: 2017??5??11??(??) 7:53
??: ""; 
: "klee-dev"; 
: Re: [klee-dev] One phenomenon after the execution using klee



Hi,

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

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

[Dan Liew]

Hi,

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