silently concretize float expression to value

[Xiaomei Hou]

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?

If I have to change the code of KLEE, could you give some suggestions?

Thanks a lot!

Best wishes!

Xiaomei

[Daniel Liew]

Post by Xiaomei Hou
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.

[Cristian Cadar]

Post by Daniel Liew

Post by Xiaomei Hou
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/

Just a quick clarification: KLEE-FP has support for floating point only
in the context of reasoning about code equivalence. See our paper for
more details: http://www.doc.ic.ac.uk/~cristic/papers/kleefp-eurosys-11.pdf

Best,
Cristian