diff options
author | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-10-25 17:27:36 +0000 |
---|---|---|
committer | Mikhail R. Gadelha <mikhail.ramalho@gmail.com> | 2018-10-25 17:27:36 +0000 |
commit | b264f83ea398d5c0131d7e31c6d814ae7ecd5b72 (patch) | |
tree | 94dbcfdcfdc54b83868904a6b20918fb91a0cc55 | |
parent | 632df14c519e15124316a6451473fbc5a52daf51 (diff) |
[analyzer] Fixed bitvector from model always being unsigned
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
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@345283 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r-- | lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp index 7faebb5f6c..e6a5f11fa1 100644 --- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -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 { |