[klee-dev] Get the conditions on a path

[sudiptac]

Hi,
     KLEE already prints test cases in SMT2 format via the option 
-write-smt2s.

     I am not sure what you mean by all the conditions in a path. If you 
are talking
     about each executed path, indeed KLEE does so via the option 
-write-smt2s.
     However, the overall formula might be simplified in the end.

     It is, however, quite easy to modify the code to print all the 
conditions (without
     simplification). Especially, check the function "fork" in 
Executor.cpp and where
     it uses addConstraint module to add all the conditions. Instead of 
addConstraint,
     you can use your own function to add all the conditions without any 
simplification.

     Hope this helps.

Regards,
Sudipta


On 05/25/2015 02:03 PM, Srijan R Shetty wrote:
> Hi,
>
> I was wondering if there was a way to obtain all the conditions which 
> occur in a path in klee's execution? Additionally, it would be superb 
> if they could be obtained in SMTLib form.
>
> Sincerely,
> Srijan R. Shetty.
>
>
> _______________________________________________
> 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