To the attention of the KLEE staff, Thanks for your reply. We are trying to analysis the constraint queries reusing opportunities in a single program and across different programs. We try to collect constraint by KLEE after optimisation like simplification and independence, but not cache. How could we achieve that?
Best regards, Meixian Chen, Andrea Aquino On Wed, Feb 19, 2014 at 10:43 AM, Andrea Aquino <[email protected]>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
