[klee-dev] Unexpected Output!

[Daniel Liew]

Hi,

You should check what happens if you use -emit-all-errors command line flags.

It's possible that an optimisation moved the klee_assume() call
outside of the if/else branch so that there is **only** one call to
the klee_assume() function in the LLVM bitcode. If that is the case
then KLEE will ignore any errors at the location if it is visited
again. The -emit-all-errors flag will cause KLEE to report all errors
even if KLEE has visited that Instruction in the LLVM bitcode before.

To see what LLVM Bitcode is interpreting take a look at
klee-last/assembly.ll file produced by KLEE.

There is probably more to this issue because I didn't expect KLEE to
generate a test case for paths with invalid constraints.

Thanks,
Dan


On 24 January 2014 15:16, General Email <general_mail2011 at yahoo.com> wrote:
> Hi,
>
> Can anybody correct me if my notice is wrong?
>
> I have the following code which should generate two symbolic execution
> paths; none of them can by satisfiable. However Klee doesn't show this!!!
>
> int main()
> {
>   int attr1=100, attr2=12;
>   int y;
>   klee_make_symbolic(&y, sizeof(int), "y");
>
>   if(y>0)
>   {
>     attr1=y+7;
>     attr2=500;
>     printf("attr2 = %d\n", attr2);
>     klee_assume(attr1<0); //by all means this cannot be satisfied
>   }
>   else
>   {
>     attr2=800;
>     printf("attr2 = %d\n", attr2);
>     klee_assume(attr1<0); ////by all means this also cannot be satisfied
>   }
> }
>
> Here is the output from Klee:
> attr2 = 800
> KLEE: ERROR: invalid klee_assume call (provably false)
> KLEE: NOTE: now ignoring this error at this location
> attr2 = 500
> //My question why it doesn't give an error saying "invalid klee_assume call
> (provably false)" here also?
> KLEE: done: total instructions = 32
> KLEE: done: completed paths = 2
> KLEE: done: generated tests = 2
>
> Here are the values of y generated in each test:
> ktest file : 'klee-last/test000001.ktest' //This represents the else branch
> (i.e., y<=0)
> object    0: name: 'y'
> object    0: size: 4
> object    0: data: 0
>
> ktest file : 'klee-last/test000002.ktest' //This represents the then branch
> (i.e., y>0)
> object    0: name: 'y'
> object    0: size: 4
> object    0: data: 2147483642
>
> Note: using klee_assert in place of klee_assume will give assertion fail in
> the two branches.
> attr2 = 800
> KLEE: ERROR: ASSERTION FAIL: attr1<0
> KLEE: NOTE: now ignoring this error at this location
> attr2 = 500
> KLEE: ERROR: ASSERTION FAIL: attr1<0
>
> Please advise?
> Thanks