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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
