[klee-dev] question about klee_print_expr

[Mingyue Jiang]

Dear All,

I intended to get the symbolic values of an variable by klee_print_expr.
There are always multiple paths are explored during symbolic execution, so more than one symbolic expression of the variable are outputted.
I assumed that the order of the outputted symbolic expressions of the variable was the same as the order of the outputted path conditions. That is, the first expression of the variable is obtain under the path condition specified in test000001.pc.
   Surprisedly,  I found that the outputted symbolic expression of the variable is not always consistent with the corresponding path condition.

  Considering following program.

   main()
  {
     int a,b;
     klee_make_symbolic(&a,sizeof(a),"a");
      if(a>0)
        b=a+10;
     else
       b=-a+10;
    klee_print_expr("b=",b);
  }
  KLEE explores two paths for the program and also gives two symbolic expressions for b:

(1)    b:=(Add w32 10 (ReadLSB w32 0 a))

(2)    b:=(Sub w32 10 (ReadLSB w32 0 a)),
If It is explicitly that the expression (1) is obtain under path condition a>0. But it seems nondeterministic, because sometimes the first path condition is a>0 but the first expression of "b" is (2).

Could anyone can help me with this problem?
If there is no relationship between the obtained symbolic expressions and path conditions, how could I know which path is related to the given symbolic expression of the variable.
Thanks.
Best regards,

Mingyue Jiang
-------------- next part --------------
HTML attachment scrubbed and removed