[klee-dev] KLEE+Z3 (an instance of KLEE-MultiSolver) still concretizes floating point expression to 0.

[Cristian Cadar]

On 20/08/15 18:40, Dan Liew wrote:
>> Is there a way to tell KLEE not to concretieze floating point expression to
>> 0 so KLEE + Z3 can be useful when handling floating point program?
>>
>
> Not right now no. KLEE's expression language does not support floating
> point constraints right now which is why floating point numbers get
> concretised. There is a fork of KLEE (KLEE-CL/KLEE-FP) that does
> support floating point numbers in its expression language
Yes, and a nice contribution to KLEE would be to add support for 
floating-point expressions, by porting those changes from 
KLEE-FP/KLEE-CL (http://srg.doc.ic.ac.uk/projects/klee-cl/)

Best,
Cristian