[klee-dev] Floating-Point Symbolic Execution

[Andrew Santosa]

Dear All,

In KLEE, it seems symbolic floating point variables are simply converted to int and grounded to 0. I am wonderingwhat is the current state of floating point symbolic execution support in KLEE? I know there has been some workon 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




-------------- next part --------------
HTML attachment scrubbed and removed