[klee-dev] How to parse (and convert) constraint expressions

[Qiao Kang]

Got it, that's very useful suggestion!

Thanks,
Qiao

On Mon, Jul 29, 2019 at 6:46 AM Cadar, Cristian <c.cadar at imperial.ac.uk>
wrote:

> As a starting point, I would look in the code for Kleaver, which
> incorporates a parser for KQuery expressions.
>
> Best,
> Cristian
>
> On 27/07/2019 23:52, Qiao Kang wrote:
> > Hi,
> >
> > I'm wondering if we can parse a constraint expression in KLEE and
> > potentially convert it to another format. For instance, given this
> > constraint: (Sle 0 (ZExt w32 (Read w8 0 a))). Is there an esay way to
> > parse it (i.e., using existing APIs) and output a string like "a >= 0"?
> > I'm only considering simple linear constraints like this one.
> >
> > Thanks,
> > Qiao
> >
> > _______________________________________________
> > 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