[PATCH] D49305: [analyzer] Fix the Z3 backend always generating unsigned APSInt

[Phabricator via Phabricator via cfe-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rC337169: [analyzer] Fix the Z3 backend always generating 
unsigned APSInt (authored by mramalho, committed by ).
Herald added a subscriber: cfe-commits.

Repository:
  rC Clang

https://reviews.llvm.org/D49305

Files:
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp


Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -681,12 +681,14 @@
       Z3_get_numeral_uint64(Z3Context::ZC, AST,
                             reinterpret_cast<__uint64 *>(&Value[0]));
       if (Sort.getBitvectorSortSize() <= 64) {
-        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true);
+        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
+                           Int.isUnsigned());
       } else if (Sort.getBitvectorSortSize() == 128) {
         Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
         Z3_get_numeral_uint64(Z3Context::ZC, AST,
                               reinterpret_cast<__uint64 *>(&Value[1]));
-        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
+        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
+                           Int.isUnsigned());
       } else {
         assert(false && "Bitwidth not supported!");
         return false;
@@ -702,7 +704,7 @@
           llvm::APInt(Int.getBitWidth(),
                       Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
                                                                          : 0),
-          true);
+          Int.isUnsigned());
       return true;
     }
   }



Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -681,12 +681,14 @@
       Z3_get_numeral_uint64(Z3Context::ZC, AST,
                             reinterpret_cast<__uint64 *>(&Value[0]));
       if (Sort.getBitvectorSortSize() <= 64) {
-        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true);
+        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
+                           Int.isUnsigned());
       } else if (Sort.getBitvectorSortSize() == 128) {
         Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
         Z3_get_numeral_uint64(Z3Context::ZC, AST,
                               reinterpret_cast<__uint64 *>(&Value[1]));
-        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
+        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
+                           Int.isUnsigned());
       } else {
         assert(false && "Bitwidth not supported!");
         return false;
@@ -702,7 +704,7 @@
           llvm::APInt(Int.getBitWidth(),
                       Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
                                                                          : 0),
-          true);
+          Int.isUnsigned());
       return true;
     }
   }

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits