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

Phabricator via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Mon Jul 16 06:37:43 PDT 2018


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;
     }
   }


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D49305.155665.patch
Type: text/x-patch
Size: 1449 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20180716/5246c1b7/attachment-0001.bin>


More information about the cfe-commits mailing list