delcypher added inline comments.
================ Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:559 + Float.toString(Chars, 0, 0); + AST = Z3_mk_numeral(Z3Context::ZC, Chars.c_str(), Sort); + break; ---------------- ddcc wrote: > delcypher wrote: > > @ddcc I'm not convinced this is a good idea. Printing as a decimal string > > could lead to rounding errors. I think you're better of getting an APInt > > from the APFloat, constructing a bitvector constant from those bits and > > then using `Z3_mk_fpa_to_fp_bv()` to get a Z3Expr of the right sort. That > > was we are being bit-wise accurate. > From the comments inside `APFloat::toString()`, this should be precise enough > to round-trip from float to string and back again with no loss of precision. > However, the I agree that bitcasting makes more sense, especially given the > overhead of string conversion. The APFloat comments claim this but[[ https://bugs.llvm.org/show_bug.cgi?id=24539 | I've found at least one case where this does not hold ]] in the current implementation. https://reviews.llvm.org/D28952 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
