[klee-dev] Unexpected Output!

[Cristian Cadar]

 From what I can tell, there's nothing to prevent y+7 from overflowing 
and become negative.

Cristian

On 24/01/14 15:16, General Email 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
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>