diff options
Diffstat (limited to 'lib/Analysis/BasicConstraintManager.cpp')
| -rw-r--r-- | lib/Analysis/BasicConstraintManager.cpp | 29 |
1 files changed, 25 insertions, 4 deletions
diff --git a/lib/Analysis/BasicConstraintManager.cpp b/lib/Analysis/BasicConstraintManager.cpp index ca97f930dd..2edbd80341 100644 --- a/lib/Analysis/BasicConstraintManager.cpp +++ b/lib/Analysis/BasicConstraintManager.cpp @@ -228,6 +228,12 @@ BasicConstraintManager::AssumeSymInt(const GRState* St, bool Assumption, else return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible); + case BinaryOperator::LT: + if (Assumption) + return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible); + else + return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible); + case BinaryOperator::LE: if (Assumption) return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible); @@ -302,15 +308,30 @@ const GRState* BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolID sym, const llvm::APSInt& V, bool& isFeasible) { - // FIXME: Primitive logic for now. Only reject a path if the value of - // sym is a constant X and !(X >= V). - + // Reject a path if the value of sym is a constant X and !(X >= V). if (const llvm::APSInt* X = getSymVal(St, sym)) { isFeasible = *X >= V; return St; } - isFeasible = true; + // 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; + return St; } |