summaryrefslogtreecommitdiff
path: root/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp')
-rw-r--r--lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp16
1 files changed, 15 insertions, 1 deletions
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index c5e0f9b862..ef2fcefb05 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -254,6 +254,21 @@ ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef State,
assert(BinaryOperator::isComparisonOp(Op) &&
"Non-comparison ops should be rewritten as comparisons to zero.");
+ SymbolRef Sym = LHS;
+
+ // Simplification: translate an assume of a constraint of the form
+ // "(exp comparison_op expr) != 0" to true into an assume of
+ // "exp comparison_op expr" to true. (And similarly, an assume of the form
+ // "(exp comparison_op expr) == 0" to true into an assume of
+ // "exp comparison_op expr" to false.)
+ if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
+ if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym)) {
+ BinaryOperator::Opcode Op = SE->getOpcode();
+ if (BinaryOperator::isComparisonOp(Op))
+ return assume(State, nonloc::SymbolVal(Sym), (Op == BO_NE ? true : false));
+ }
+ }
+
// Get the type used for calculating wraparound.
BasicValueFactory &BVF = getBasicVals();
APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
@@ -265,7 +280,6 @@ ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef State,
// x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
// in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
// the subclasses of SimpleConstraintManager to handle the adjustment.
- SymbolRef Sym = LHS;
llvm::APSInt Adjustment = WraparoundType.getZeroValue();
computeAdjustment(Sym, Adjustment);