Right now, the floating point unit (fpu/softfloat.c) is compiled to LLVM IR, and linked into the LLVM module where all helper code and generated translation block code lives. If floating point support is desired, it would be a good idea to check
whether the current floating point support is working (it most likely requires some tweaking in s2e::S2EExecutor::cleanModule to not remove required functions from the module)
whether a KLEE and a constraint solver, e.g., Z3, support floating point and the floating point helper functions can be replaced by native helper functions (SpecialFunctionHandlers in s2e::S2EExecutor, like handlerBaseInstruction)
Right now, the floating point unit (fpu/softfloat.c) is compiled to LLVM IR, and linked into the LLVM module where all helper code and generated translation block code lives. If floating point support is desired, it would be a good idea to check