[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

[Dan Liew via Phabricator via cfe-commits]

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