Hi Andrew,
KLEE-FP/KLEE-CL (https://srg.doc.ic.ac.uk/projects/klee-cl/) is targeted
primarily toward cross-checking of (purportedly) equivalent FP code,
although it has some basic integration with a FP solver from CBMC.
Dan Liew, Alastair Donaldson and I are working on full FP support for
KLEE on top of Z3, but this is still work in progress. I don't
anticipate having anything ready until the end of the year.
Best,
Cristian
On 27/05/16 14:42, Andrew Santosa wrote:
Dear All,
In KLEE, it seems symbolic floating point variables are simply converted
to int and grounded to 0. I am wondering
what is the current state of floating point symbolic execution support
in KLEE? I know there has been some work
on KLEE-FP in the past, but does it actually check path feasibility via
path condition satisfiability in QF_FPA?
Now that KLEE supports Z3 as backend solver, perhaps such feasibility
checking is not too difficult to implement?
Best,
Andrew
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
