[klee-dev] Replay path condition

[Cristian Cadar]

The .pc file uses our own constraint language, which is described at
https://klee.github.io/docs/kquery/.  As Martin said, our tool Kleaver
(/tools/kleaver/) can already parse these constraints and construct the
corresponding KLEE expressions, so that would be the starting point.

Best,
Cristian

On 20/04/2015 11:35, Martin Nowack wrote:
> Have a look at tools/kleaver - this should give you an idea how to proceed.
> 
> Cheers,
> Martin
>> On 20 Apr 2015, at 06:06, Mohammad Wamiq Saifi <wamiqsaifi at gmail.com> wrote:
>>
>> 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
>>
>> _______________________________________________
>> 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
>