[analyzer] Fixed bitvector from model always being unsigned
authorMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Thu, 25 Oct 2018 17:27:36 +0000 (17:27 +0000)
committerMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Thu, 25 Oct 2018 17:27:36 +0000 (17:27 +0000)
Summary:
Getting an `APSInt` from the model always returned an unsigned integer because of the unused parameter.

This was not breaking any test case because no code relies on the actual value of the integer returned here, but rather it is only used to check if a symbol has more than one solution in `getSymVal`.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin, Szelethus, donat.nagy, dkrupp

Differential Revision: https://reviews.llvm.org/D53637

llvm-svn: 345283

clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

index 7faebb5..e6a5f11 100644 (file)
@@ -733,9 +733,11 @@ public:
 
   llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
                             bool isUnsigned) override {
-    return llvm::APSInt(llvm::APInt(
-        BitWidth, Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
-        10));
+    return llvm::APSInt(
+        llvm::APInt(BitWidth,
+                    Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
+                    10),
+        isUnsigned);
   }
 
   bool getBoolean(const SMTExprRef &Exp) override {