[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