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

[Cadar, Cristian]

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
>