[klee-dev] How to Interpret Klee Path Predicate

[Dan Liew]

On 21 Mar 2016 11:19 a.m., "Dan Liew" <dan at su-root.co.uk> wrote:
>
>
> On 21 Mar 2016 10:33 a.m., "Azizul Hakim" <azizulfahim2002 at gmail.com>
wrote:
> >
> > How do we interpret the path predicates generated by KLEE. I've the
following path predicates generated by S2E tool which uses KLEE. This
predicate is generated from one branch of an IF-ELSE statement.
> >
>
> IIRC you're looking at STP's internal format which I think is based on
CVC's internal format
>
> http://cvc4.cs.nyu.edu/wiki/CVC4%27s_native_language
>
> Mainline KLEE supports emitting constraints in the SMT-LIBv2 format which
is more widely used and documented. However I don't know when S2E forked
from KLEE so I find know if S2E has this capability

Sorry phone autocorrected incorrectly. It should say

However I don't know when S2E forked from KLEE so I don't know if S2E has
this capability.
-------------- next part --------------
HTML attachment scrubbed and removed