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 <[email protected]>
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
[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
