[klee-dev] silently concretize float expression to value

[Daniel Liew]

On 28 February 2013 15:07, Xiaomei Hou <hxm815190908 at gmail.com> 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.