On 28 February 2013 15:07, Xiaomei Hou <[email protected]> wrote: > Hi, > > KLEE silently concretizes expression to value, when expression is floating > point. > > KLEE: WARNING: silently concretizing (reason: floating point) expression > (ReadLSB w32 0 dDA) to value 56 (:0) > > I want to work with examples that has float. Can KLEE deal with this?
KLEE cannot currently handle symbolic floating point expressions. A fork KLEE called KLEE-FP can handle symbolic floating point expressions. See http://www.pcc.me.uk/~peter/klee-fp/ Regards, Dan Liew. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
