diff options
| -rw-r--r-- | lib/Analysis/BasicConstraintManager.cpp | 26 | ||||
| -rw-r--r-- | test/Analysis/null-deref-ps.c | 9 |
2 files changed, 32 insertions, 3 deletions
diff --git a/lib/Analysis/BasicConstraintManager.cpp b/lib/Analysis/BasicConstraintManager.cpp index c8065d1869..f4290ffb67 100644 --- a/lib/Analysis/BasicConstraintManager.cpp +++ b/lib/Analysis/BasicConstraintManager.cpp @@ -328,6 +328,13 @@ const GRState* BasicConstraintManager::AssumeSymGT(const GRState* St, SymbolID sym, const llvm::APSInt& V, bool& isFeasible) { + // Is 'V' the largest possible value? + if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isSigned())) { + // sym cannot be any value greater than 'V'. This path is infeasible. + isFeasible = false; + return St; + } + // FIXME: For now have assuming x > y be the same as assuming sym != V; return AssumeSymNE(St, sym, V, isFeasible); } @@ -341,10 +348,23 @@ BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolID sym, isFeasible = *X >= V; return St; } + + // Sym is not a constant, but it is worth looking to see if V is the + // maximum integer value. + if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isSigned())) { + // If we know that sym != V, then this condition is infeasible since + // there is no other value greater than V. + isFeasible = !isNotEqual(St, sym, V); + + // If the path is still feasible then as a consequence we know that + // 'sym == V' because we cannot have 'sym > V' (no larger values). + // Add this constraint. + if (isFeasible) + return AddEQ(St, sym, V); + } + else + isFeasible = true; - isFeasible = !isNotEqual(St, sym, V) || - (V != llvm::APSInt::getMaxValue(V.getBitWidth(), V.isSigned())); - return St; } diff --git a/test/Analysis/null-deref-ps.c b/test/Analysis/null-deref-ps.c index eb6062b981..c3bf444420 100644 --- a/test/Analysis/null-deref-ps.c +++ b/test/Analysis/null-deref-ps.c @@ -144,3 +144,12 @@ void f11(unsigned i) { } } +void f11b(unsigned i) { + int *x = 0; + if (i <= ~(unsigned)0) { + // always true + } else { + *x = 42; // no-warning + } +} + |