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

[Cristian Cadar]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>