Hi Leandro, Vijay, We are currently experimenting with starting execution from a set of concrete inputs; we can share our results and changes once we are done.
There is actually already some support for this in the open-source version of KLEE: just grep the help options for the "seed" functionality. Cristian On 29/06/11 08:10, Leandro Sales wrote: > 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 >>> >>> >> > > > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
