[klee-dev] Replay path condition

Martin Nowack martin_nowack at tu-dresden.de
Mon Apr 20 11:35:43 BST 2015


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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150420/dc666452/attachment.sig>


More information about the klee-dev mailing list