From a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4 Mon Sep 17 00:00:00 2001 From: Zhongxing Xu Date: Wed, 25 Mar 2009 05:58:37 +0000 Subject: This patch adds two more SymbolData subclasses: SymIntExpr and SymSymExpr, for representing symbolic expressions like 'x'+3 and 'x'+'y'. The design is subjected to change later when we fix the class hierarchy of symbolic expressions. git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@67678 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Analysis/SimpleConstraintManager.cpp | 33 +++++++++++--------------------- 1 file changed, 11 insertions(+), 22 deletions(-) (limited to 'lib/Analysis/SimpleConstraintManager.cpp') diff --git a/lib/Analysis/SimpleConstraintManager.cpp b/lib/Analysis/SimpleConstraintManager.cpp index e6f940e57c..50552c1144 100644 --- a/lib/Analysis/SimpleConstraintManager.cpp +++ b/lib/Analysis/SimpleConstraintManager.cpp @@ -21,28 +21,11 @@ namespace clang { SimpleConstraintManager::~SimpleConstraintManager() {} bool SimpleConstraintManager::canReasonAbout(SVal X) const { - if (nonloc::SymIntConstraintVal *Y = dyn_cast(&X)) { - const SymIntConstraint& C = Y->getConstraint(); - switch (C.getOpcode()) { - // We don't reason yet about bitwise-constraints on symbolic values. - case BinaryOperator::And: - case BinaryOperator::Or: - case BinaryOperator::Xor: - return false; - // We don't reason yet about arithmetic constraints on symbolic values. - case BinaryOperator::Mul: - case BinaryOperator::Div: - case BinaryOperator::Rem: - case BinaryOperator::Add: - case BinaryOperator::Sub: - case BinaryOperator::Shl: - case BinaryOperator::Shr: - return false; - - // All other cases. - default: - return true; - } + if (nonloc::SymbolVal* SymVal = dyn_cast(&X)) { + const SymbolData& data + = getSymbolManager().getSymbolData(SymVal->getSymbol()); + return !(data.getKind() == SymbolData::SymIntKind || + data.getKind() == SymbolData::SymSymKind ); } return true; @@ -143,6 +126,12 @@ SimpleConstraintManager::Assume(const GRState* St, NonLoc Cond, bool Assumption, const GRState* SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond, bool Assumption, bool& isFeasible) { + // We cannot reason about SymIntExpr and SymSymExpr. + if (!canReasonAbout(Cond)) { + isFeasible = true; + return St; + } + BasicValueFactory& BasicVals = StateMgr.getBasicVals(); SymbolManager& SymMgr = StateMgr.getSymbolManager(); -- cgit v1.2.3-70-g09d2