You simply need to pass the --write-pcs, write-cvcs or write-smt2s
flags, see http://klee.github.io/klee/klee-files.html for more details.
Best,
Cristian
On 19/02/14 09:43, Andrea Aquino wrote:
To the attention of the KLEE staff,
first of all we would like to introduce ourselves.
My name is Andrea Aquino while my colleague’s name is Meixian Chen, we are
Ph.D. students at Università della Svizzera Italiana (Switzerland, Ticino).
We are currently looking for a way to extract path conditions produced by KLEE.
Actually we will need to save on disk the symbolic constraints produced by KLEE
during its execution in a human readable format.
For example if analysing a program KLEE calculates 3 path conditions:
1. x > 0
2. y > 0 && y < 5
3. x + y < 10
we would like to store them in a file in order to perform a posteriori checks
on them.
We don’t care about redundancy (the same constraint stored two or more times).
Is there an easy way to achieve this goal?
How can we proceed?
Best regards,
Andrea Aquino, Meixian Chen
_______________________________________________
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
