[klee-dev] How to get only path conditions in human friendly mode?

[Andrew Santosa]

Dear Javier,
I think you can use -write-pcs to make KLEE output test*.pc files which showthe path condition for each generated test.
-write-pcs will ouput in KLEE's own expression format, but other formats arealso avaiable: -write-smt2s and -write-cvcs will output in SMT2 and CVC formatrespectively.
Best,Andrew
 

    On Saturday, 3 December 2016, 21:32, Javier Godoy <j.godoy277 at gmail.com> wrote:
 

 Hi!

Is possible with Klee get only all path conditions from a symbolic execution over a method?

Example: For the next method, i need to obtain "(x+1 > 0)" and "(x+1 <= 0)".
void m(int x){   int a = x + 1;   if a > 0      print 1;   else       print 0;}
Thanks!!! :)
_______________________________________________
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