diff options
| -rw-r--r-- | lib/Analysis/BasicConstraintManager.cpp | 27 | ||||
| -rw-r--r-- | test/Analysis/null-deref-ps.c | 8 |
2 files changed, 11 insertions, 24 deletions
diff --git a/lib/Analysis/BasicConstraintManager.cpp b/lib/Analysis/BasicConstraintManager.cpp index 9ff44e0112..0576eaf2a1 100644 --- a/lib/Analysis/BasicConstraintManager.cpp +++ b/lib/Analysis/BasicConstraintManager.cpp @@ -320,24 +320,9 @@ BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolID sym, return St; } - // sym is not a constant, but it might be not-equal to a constant. - // Observe: V >= sym is the same as sym <= V. - // check: is sym != V? - // check: is sym > V? - // if both are true, the path is infeasible. - - if (isNotEqual(St, sym, V)) { - // Is sym > V? - // - // We're not doing heavy range analysis yet, so all we can accurately - // reason about are the edge cases. - // - // If V == 0, since we know that sym != V, we also know that sym > V. - isFeasible = V != 0; - } - else - isFeasible = true; - + isFeasible = !isNotEqual(St, sym, V) || + (V != llvm::APSInt::getMaxValue(V.getBitWidth(), V.isSigned())); + return St; } @@ -352,8 +337,10 @@ BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolID sym, isFeasible = *X <= V; return St; } - - isFeasible = true; + + isFeasible = !isNotEqual(St, sym, V) || + (V != llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned())); + return St; } diff --git a/test/Analysis/null-deref-ps.c b/test/Analysis/null-deref-ps.c index 0f86acdabc..1fdcd06d43 100644 --- a/test/Analysis/null-deref-ps.c +++ b/test/Analysis/null-deref-ps.c @@ -91,21 +91,21 @@ int f8(int *p, int *q) { int* qux(); -int f9(int len) { +int f9(unsigned len) { assert (len != 0); int *p = 0; - for (int i = 0; i < len; ++i) + for (unsigned i = 0; i < len; ++i) p = qux(i); return *p++; // no-warning } -int f9b(int len) { +int f9b(unsigned len) { assert (len > 0); // note use of '>' int *p = 0; - for (int i = 0; i < len; ++i) + for (unsigned i = 0; i < len; ++i) p = qux(i); return *p++; // no-warning |