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
[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
