[klee-dev] Symbolic Expression for Variable

[Andrew Santosa]

 Hi Ridwan,
I think you can do this using klee_print_expr() without modifying KLEE.For example (from [klee-dev] question about klee_print_expr):

| 
| 
|  | 
[klee-dev] question about klee_print_expr


 |

 |

 |




#include <klee/klee.h>

int main(int arc, char **argv)
  {
     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);
    return 0;
  }

Running KLEE with this program as input gives you the following output:
$ klee example.bc
KLEE: output directory is "/home/dcsandr/projects/klee/klee-out-0"
KLEE: Using STP solver backend
b=:(Add w32 10
          (ReadLSB w32 0 a))
b=:(Sub w32 10
          (ReadLSB w32 0 a))

KLEE: done: total instructions = 27
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

Each printed value of b represetns the valueof b at the end of one of the two execution paths.
I hope that helps.
Best,Andrew

    On Thursday, 31 May 2018, 2:30:03 PM SGT, Ridwan Shariffdeen <rshariffdeen at gmail.com> wrote:  
 
 Hi
I want to obtain the symbolic expression for a given variable at the end of an execution of a program. Is this possible with the current implementation? or do I need to modify klee for this? If so can you point out in which direction I should look into?
Appreciate any help in this regards
Thanks!Ridwan

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
  
-------------- next part --------------
HTML attachment scrubbed and removed