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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
