delcypher added inline comments.
================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:619
+
+ llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true);
+ Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);
----------------
@ddcc Why use APSInt here? Why not APInt, we are looking at raw bits and don't
want to interpret the most significant bit in a special way.
================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:668
+ default:
+ llvm_unreachable("Unsupported sort to integer!");
+ case Z3_BV_SORT: {
----------------
Is `Z3_FLOATING_POINT_SORT` possible in your 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
