From 0a41e5a03a2753e736dece6fc6847e6de2dedec1 Mon Sep 17 00:00:00 2001 From: Ted Kremenek Date: Fri, 19 Sep 2008 18:00:36 +0000 Subject: Fixed logic error in BasicConstraintManager pointed out by Zhongxing Xu. For checking if a symbol >= value, we need to check if symbol == value || symbol > value. When checking symbol > value and we know that symbol != value, the path is infeasible only if value == maximum integer. For checking if a symbol <= value, we need to check if symbol == value || symbol < value. When checking symbol < value and we know that symbol != value, the path is infeasible only if value == minimum integer. Updated test case exercising this logic: we only prune paths if the values are unsigned. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@56354 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Analysis/BasicConstraintManager.cpp | 27 +++++++-------------------- 1 file changed, 7 insertions(+), 20 deletions(-) (limited to 'lib/Analysis/BasicConstraintManager.cpp') 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; } -- cgit v1.2.3-18-g5258