Klee uses STP as its constraint solver, but theoretically it is possible to change its solver. STP does not allow floating point operations. If we decide to replace STP with another constraint solver, say z3, would klee be able to generate floating point constraints?
The flow is: C code -> llvm bitcode -> klee -> stp clauses -> klee -> output
If klee gets floating point llvm instructions, is it able to interpret them? Does it generate fp constraints in smt language, that stp is not able to handle them, or it doesn't generate fp constraints at all?
Any reference for your answer would be appreciated.
This link contains a fork of KLEE with floating point support. No idea how mature is it, though.