[klee-dev] Unexpected Output!

[General Email]

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