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.godoy...@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@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev