aboutsummaryrefslogtreecommitdiff
path: root/lib/Analysis/GRExprEngine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Analysis/GRExprEngine.cpp')
-rw-r--r--lib/Analysis/GRExprEngine.cpp26
1 files changed, 25 insertions, 1 deletions
diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp
index d00bfe640a..4b540e78d5 100644
--- a/lib/Analysis/GRExprEngine.cpp
+++ b/lib/Analysis/GRExprEngine.cpp
@@ -2674,9 +2674,33 @@ void GRExprEngine::VisitUnaryOperator(UnaryOperator* U, NodeTy* Pred,
SVal Result = EvalBinOp(Op, V2, MakeConstantVal(1U, U), U->getType());
// Conjure a new symbol if necessary to recover precision.
- if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result))
+ if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result)){
Result = ValMgr.getConjuredSymbolVal(Ex,
Builder->getCurrentBlockCount());
+
+ // If the value is a location, ++/-- should always preserve
+ // non-nullness. Check if the original value was non-null, and if so propagate
+ // that constraint.
+ if (Loc::IsLocType(U->getType())) {
+ SVal Constraint = EvalBinOp(BinaryOperator::EQ, V2,
+ ValMgr.makeZeroVal(U->getType()),
+ getContext().IntTy);
+
+ bool isFeasible = false;
+ Assume(state, Constraint, true, isFeasible);
+ if (!isFeasible) {
+ // It isn't feasible for the original value to be null.
+ // Propagate this constraint.
+ Constraint = EvalBinOp(BinaryOperator::EQ, Result,
+ ValMgr.makeZeroVal(U->getType()),
+ getContext().IntTy);
+
+ bool isFeasible = false;
+ state = Assume(state, Constraint, false, isFeasible);
+ assert(isFeasible && state);
+ }
+ }
+ }
state = BindExpr(state, U, U->isPostfix() ? V2 : Result);