[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: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