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 <[email protected]> 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" <[email protected]> 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 <[email protected]> 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 >>> [email protected] >>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >>> >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
