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.

llvm-svn: 67678

1 files changed, 11 insertions, 22 deletions

diff --git a/clang/lib/Analysis/SimpleConstraintManager.cpp b/clang/lib/Analysis/SimpleConstraintManager.cpp
index e6f940e57cc..50552c11440 100644
--- a/clang/lib/Analysis/SimpleConstraintManager.cpp
+++ b/clang/lib/Analysis/SimpleConstraintManager.cpp
@@ -21,28 +21,11 @@ namespace clang {
 SimpleConstraintManager::~SimpleConstraintManager() {}
 
 bool SimpleConstraintManager::canReasonAbout(SVal X) const {
-  if (nonloc::SymIntConstraintVal *Y = dyn_cast<nonloc::SymIntConstraintVal>(&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<nonloc::SymbolVal>(&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();