Thanks Vijay. For your better explanation of my question. @David, my problem is a little more complex then just saying Klee to write path-constraints. Maybe I was not completely clear in my question. I want to go in the "reverse" way that Klee usually goes. Instead of executing my program symbolically, extract path constraints (.pc) and get a solution (.ktest), I want to find the path constraints based on a ktest file (that represents my input), that I have already generated.
Is that possible? Thanks, Leandro On Wed, Jun 29, 2011 at 4:45 AM, Vijay Ganesh <hellovijay at gmail.com> wrote: > Hi, > > Generalizing on Leonardo's question: > > Have there been extensive experiments using KLEE in the whitebox > fuzzing mode (similar to SAGE), i.e., using a seed set of inputs to > extract paths, and then solving them (typically offline) to explore > branches on these paths? The goal here is to look for deep errors, as > opposed to the typical usage-scenario of coverage. > > Thanks, > Vijay Ganesh. > > On Tue, Jun 28, 2011 at 3:21 PM, Leandro Sales <leandro.shp at gmail.com> > wrote: > > Hi, > > Is there a way to use klee to extract the path condition followed for a > > given input (or file)? > > thanks, > > Leandro > > _______________________________________________ > > klee-dev mailing list > > klee-dev at keeda.stanford.edu > > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > > > > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110629/5baf89c9/attachment.html
