Fix: <rdar://problem/6777209> false Dereference of null pointer in loop: pointer increment/decrement preserves non-nullness
When the StoreManager doesn't reason well about pointer-arithmetic, propagate
the non-nullness constraint on a pointer value when performing pointer
arithmetic uisng ++/--.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@69741 91177308-0d34-0410-b5e6-96231b3b80d8
diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp
index d00bfe6..4b540e7 100644
--- a/lib/Analysis/GRExprEngine.cpp
+++ b/lib/Analysis/GRExprEngine.cpp
@@ -2674,9 +2674,33 @@
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);