[klee-dev] How to Interpret Klee Path Predicate
Dan Liew
dan at su-root.co.uk
Mon Apr 4 22:53:30 BST 2016
On 4 April 2016 at 17:55, Azizul Hakim <azizulfahim2002 at gmail.com> wrote:
> Thanks Dan. I can also print the constraints in the format below. Do you
> happen to have any idea where I can get a documentation of this format?
>
>
>
> (query [(Eq false
> (Eq (w32 0x0)
> (And w32 (Add w32 (w32 0xfffffffe)
> (ZExt w32 (Read w8 0x0 v0_str_0)))
> (w32 0xff))))]
> false)
>
>
>
> Thanks for your time.
>
That is the [kQuery format](https://klee.github.io/docs/kquery/) which
is specific to KLEE. One thing you could try doing is porting the
ExprSMTLIBPrinter to your fork of KLEE, it shouldn't be too difficult.
More information about the klee-dev
mailing list