delcypher added inline comments.
================ Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:674 + // are the same size. + Z3_get_numeral_uint64(Z3Context::ZC, AST, + reinterpret_cast<__uint64 *>(&Value)); ---------------- ddcc wrote: > The only problem I see now is that if a IEEEquad is fed in, it will generate > a 128-bit bitvector, which will be truncated at this point. But the z3 API > doesn't support retrieving a rational into anything larger than 64-bit, so > perhaps converting it to string is the way to go here. @ddcc I'm heavily against using the string method due to rounding problems it might introduce. The trick to handling types wider than 64 bits is to construct a new Z3_ast that does an `Z3_mk_extract()` to pull out the bits you want and then call `Z3_get_numeral_uint64()` on that. In the case of IEEE-754 quad you would need to pull out the lower order bits and then the higher order bits, then put these into an array and build an `APInt` from that. https://reviews.llvm.org/D28952 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
