[klee-dev] Replay path condition

[Mohammad Wamiq Saifi]

Yes, It would be a nice addon to klee.

@Cristian, The .pc file contains the path conditions in smtlib format. Is
there a mechanism already in klee which converts it back to the klee's
internal data structure? Can you shed some light on how to proceed for it?

Best,
Wamiq
On Apr 19, 2015 8:48 AM, "Srijan R Shetty" <srijan.shetty at gmail.com> wrote:

> Hey Cristian,
>
> Could you give me some pointers as to how to proceed with the
> implementation and where all I might have to look?
>
> Best,
> Shetty
>
> On Sun, 19 Apr 2015 at 03:35 Cristian Cadar <c.cadar at imperial.ac.uk>
> wrote:
>
>> No, but this would be a nice feature to have, and I'd be happy to accept
>> a pull request.  Essentially, one would need to assume every constraint
>> in a given .pc file when KLEE starts -- all the required mechanisms are
>> there, but they would need to be combined accordingly.
>>
>> Best,
>> Cristian
>>
>> On 18/04/2015 13:21, Srijan R Shetty wrote:
>> > Hi,
>> >
>> > I was wondering whether it was possible to replay a path condition in
>> > klee just like the --replay-path?
>> >
>> > Sincerely,
>> > Srijan R Shetty
>> >
>> >
>> > _______________________________________________
>> > klee-dev mailing list
>> > klee-dev at imperial.ac.uk
>> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>> >
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed