[klee-dev] About KLEE, how to extract path conditions

[Andrea Aquino]

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