Move GRTransferFunc* into ValueStateManager, and move the assumption logic there as well.

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@53743 91177308-0d34-0410-b5e6-96231b3b80d8

5 files changed, 245 insertions, 230 deletions

diff --git a/include/clang/Analysis/PathSensitive/GRExprEngine.h b/include/clang/Analysis/PathSensitive/GRExprEngine.h
index bb805ba092..a54b3d7ce5 100644
--- a/include/clang/Analysis/PathSensitive/GRExprEngine.h
+++ b/include/clang/Analysis/PathSensitive/GRExprEngine.h
@@ -70,10 +70,6 @@ protected:
   /// ValueMgr - Object that manages the data for all created RVals.
   BasicValueFactory& BasicVals;
   
-  /// TF - Object that represents a bundle of transfer functions
-  ///  for manipulating and creating RVals.
-  GRTransferFuncs* TF;
-  
   /// BugTypes - Objects used for reporting bugs.
   typedef std::vector<BugType*> BugTypeSet;
   BugTypeSet BugTypes;
@@ -187,6 +183,8 @@ public:
   /// getCFG - Returns the CFG associated with this analysis.
   CFG& getCFG() { return G.getCFG(); }
   
+  GRTransferFuncs& getTF() { return *StateMgr.TF; }
+  
   /// setTransferFunctions
   void setTransferFunctions(GRTransferFuncs* tf);
 
@@ -371,7 +369,7 @@ public:
   /// ProcessEndPath - Called by GRCoreEngine.  Used to generate end-of-path
   ///  nodes when the control reaches the end of a function.
   void ProcessEndPath(EndPathNodeBuilder& builder) {
-    TF->EvalEndPath(*this, builder);
+    getTF().EvalEndPath(*this, builder);
   }
   
   ValueStateManager& getStateManager() { return StateMgr; }
@@ -433,39 +431,14 @@ protected:
   ///  is true or false.
   const ValueState* Assume(const ValueState* St, RVal Cond, bool Assumption,
                            bool& isFeasible) {
-    
-    if (Cond.isUnknown()) {
-      isFeasible = true;
-      return St;
-    }
-    
-    if (isa<LVal>(Cond))
-      return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
-    else
-      return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
+    return StateMgr.Assume(St, Cond, Assumption, isFeasible);
   }
   
   const ValueState* Assume(const ValueState* St, LVal Cond, bool Assumption,
-                           bool& isFeasible);
-                     
-  const ValueState* AssumeAux(const ValueState* St, LVal Cond, bool Assumption,
-                              bool& isFeasible);
+                           bool& isFeasible) {
+    return StateMgr.Assume(St, Cond, Assumption, isFeasible);
+  }
 
-  const ValueState* Assume(const ValueState* St, NonLVal Cond, bool Assumption,
-                           bool& isFeasible);
-  
-  const ValueState* AssumeAux(const ValueState* St, NonLVal Cond,
-                              bool Assumption, bool& isFeasible);
-  
-  const ValueState* AssumeSymNE(const ValueState* St, SymbolID sym,
-                                const llvm::APSInt& V, bool& isFeasible);
-  
-  const ValueState* AssumeSymEQ(const ValueState* St, SymbolID sym,
-                                const llvm::APSInt& V, bool& isFeasible);
-  
-  const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,
-                                 const SymIntConstraint& C, bool& isFeasible);
-  
   NodeTy* MakeNode(NodeSet& Dst, Stmt* S, NodeTy* Pred, const ValueState* St) {
     assert (Builder && "GRStmtNodeBuilder not present.");
     return Builder->MakeNode(Dst, S, Pred, St);
@@ -560,25 +533,25 @@ protected:
       return X;
     
     if (isa<LVal>(X))
-      return TF->EvalCast(*this, cast<LVal>(X), CastT);
+      return getTF().EvalCast(*this, cast<LVal>(X), CastT);
     else
-      return TF->EvalCast(*this, cast<NonLVal>(X), CastT);
+      return getTF().EvalCast(*this, cast<NonLVal>(X), CastT);
   }
   
   RVal EvalMinus(UnaryOperator* U, RVal X) {
-    return X.isValid() ? TF->EvalMinus(*this, U, cast<NonLVal>(X)) : X;
+    return X.isValid() ? getTF().EvalMinus(*this, U, cast<NonLVal>(X)) : X;
   }
   
   RVal EvalComplement(RVal X) {
-    return X.isValid() ? TF->EvalComplement(*this, cast<NonLVal>(X)) : X;
+    return X.isValid() ? getTF().EvalComplement(*this, cast<NonLVal>(X)) : X;
   }
 
   RVal EvalBinOp(BinaryOperator::Opcode Op, NonLVal L, RVal R) {
-    return R.isValid() ? TF->EvalBinOp(*this, Op, L, cast<NonLVal>(R)) : R;
+    return R.isValid() ? getTF().EvalBinOp(*this, Op, L, cast<NonLVal>(R)) : R;
   }
   
   RVal EvalBinOp(BinaryOperator::Opcode Op, NonLVal L, NonLVal R) {
-    return R.isValid() ? TF->EvalBinOp(*this, Op, L, R) : R;
+    return R.isValid() ? getTF().EvalBinOp(*this, Op, L, R) : R;
   }
   
   RVal EvalBinOp(BinaryOperator::Opcode Op, RVal L, RVal R) {
@@ -591,9 +564,9 @@ protected:
 
     if (isa<LVal>(L)) {
       if (isa<LVal>(R))
-        return TF->EvalBinOp(*this, Op, cast<LVal>(L), cast<LVal>(R));
+        return getTF().EvalBinOp(*this, Op, cast<LVal>(L), cast<LVal>(R));
       else
-        return TF->EvalBinOp(*this, Op, cast<LVal>(L), cast<NonLVal>(R));
+        return getTF().EvalBinOp(*this, Op, cast<LVal>(L), cast<NonLVal>(R));
     }
 
     if (isa<LVal>(R)) {
@@ -603,10 +576,10 @@ protected:
       assert (Op == BinaryOperator::Add || Op == BinaryOperator::Sub);
 
       // Commute the operands.
-      return TF->EvalBinOp(*this, Op, cast<LVal>(R), cast<NonLVal>(L));
+      return getTF().EvalBinOp(*this, Op, cast<LVal>(R), cast<NonLVal>(L));
     }
     else
-      return TF->EvalBinOp(*this, Op, cast<NonLVal>(L), cast<NonLVal>(R));
+      return getTF().EvalBinOp(*this, Op, cast<NonLVal>(L), cast<NonLVal>(R));
   }
   
   void EvalBinOp(ExplodedNodeSet<ValueState>& Dst, Expr* E,
@@ -615,12 +588,12 @@ protected:
   
   void EvalCall(NodeSet& Dst, CallExpr* CE, RVal L, NodeTy* Pred) {
     assert (Builder && "GRStmtNodeBuilder must be defined.");
-    TF->EvalCall(Dst, *this, *Builder, CE, L, Pred);
+    getTF().EvalCall(Dst, *this, *Builder, CE, L, Pred);
   }
   
   void EvalObjCMessageExpr(NodeSet& Dst, ObjCMessageExpr* ME, NodeTy* Pred) {
     assert (Builder && "GRStmtNodeBuilder must be defined.");
-    TF->EvalObjCMessageExpr(Dst, *this, *Builder, ME, Pred);
+    getTF().EvalObjCMessageExpr(Dst, *this, *Builder, ME, Pred);
   }
   
   void EvalStore(NodeSet& Dst, Expr* E, NodeTy* Pred, const ValueState* St,
diff --git a/include/clang/Analysis/PathSensitive/GRTransferFuncs.h b/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
index e5fa069c45..b57244ae04 100644
--- a/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
+++ b/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
@@ -108,8 +108,7 @@ public:
                                const ValueState* St,
                                const ValueStateManager::DeadSymbolsTy& Dead) {}
   
-  // Return statements.
-  
+  // Return statements.  
   virtual void EvalReturn(ExplodedNodeSet<ValueState>& Dst,
                           GRExprEngine& Engine,
                           GRStmtNodeBuilder<ValueState>& Builder,
@@ -118,7 +117,7 @@ public:
 
   // Assumptions.
   
-  virtual const ValueState* EvalAssume(GRExprEngine& Engine,
+  virtual const ValueState* EvalAssume(ValueStateManager& VMgr,
                                        const ValueState* St,
                                        RVal Cond, bool Assumption,
                                        bool& isFeasible) {
diff --git a/include/clang/Analysis/PathSensitive/ValueState.h b/include/clang/Analysis/PathSensitive/ValueState.h
index 1a571f3c29..c508d6f4cd 100644
--- a/include/clang/Analysis/PathSensitive/ValueState.h
+++ b/include/clang/Analysis/PathSensitive/ValueState.h
@@ -41,6 +41,7 @@
 namespace clang {
 
 class ValueStateManager;
+class GRTransferFuncs;
   
 //===----------------------------------------------------------------------===//
 // ValueState- An ImmutableMap type Stmt*/Decl*/Symbols to RVals.
@@ -217,6 +218,10 @@ private:
   
   /// cfg - The CFG for the analyzed function/method.
   CFG& cfg;
+    
+  /// TF - Object that represents a bundle of transfer functions
+  ///  for manipulating and creating RVals.
+  GRTransferFuncs* TF;
   
 private:
 
@@ -322,6 +327,44 @@ public:
 
   const ValueState* AddNE(const ValueState* St, SymbolID sym,
                           const llvm::APSInt& V);
+  
+  // Assumption logic.
+  const ValueState* Assume(const ValueState* St, RVal Cond, bool Assumption,
+                           bool& isFeasible) {
+    
+    if (Cond.isUnknown()) {
+      isFeasible = true;
+      return St;
+    }
+    
+    if (isa<LVal>(Cond))
+      return Assume(St, cast<LVal>(Cond), Assumption, isFeasible);
+    else
+      return Assume(St, cast<NonLVal>(Cond), Assumption, isFeasible);
+  }
+  
+  const ValueState* Assume(const ValueState* St, LVal Cond, bool Assumption,
+                           bool& isFeasible);
+
+  const ValueState* Assume(const ValueState* St, NonLVal Cond, bool Assumption,
+                           bool& isFeasible);
+
+private:  
+  const ValueState* AssumeAux(const ValueState* St, LVal Cond, bool Assumption,
+                              bool& isFeasible);
+  
+  
+  const ValueState* AssumeAux(const ValueState* St, NonLVal Cond,
+                              bool Assumption, bool& isFeasible);
+  
+  const ValueState* AssumeSymNE(const ValueState* St, SymbolID sym,
+                                const llvm::APSInt& V, bool& isFeasible);
+  
+  const ValueState* AssumeSymEQ(const ValueState* St, SymbolID sym,
+                                const llvm::APSInt& V, bool& isFeasible);
+  
+  const ValueState* AssumeSymInt(const ValueState* St, bool Assumption,
+                                 const SymIntConstraint& C, bool& isFeasible);
 };
   
 } // end clang namespace
diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp
index 5159f4a4cd..c4278b1e5b 100644
--- a/lib/Analysis/GRExprEngine.cpp
+++ b/lib/Analysis/GRExprEngine.cpp
@@ -123,7 +123,6 @@ GRExprEngine::GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx,
     StateMgr(G.getContext(), CreateBasicStoreManager(G.getAllocator()),
              G.getAllocator(), G.getCFG()),
     BasicVals(StateMgr.getBasicValueFactory()),
-    TF(NULL), // FIXME
     SymMgr(StateMgr.getSymbolManager()),
     CurrentStmt(NULL),
   NSExceptionII(NULL), NSExceptionInstanceRaiseSelectors(NULL),
@@ -178,8 +177,8 @@ void GRExprEngine::EmitWarnings(BugReporterData& BRData) {
 }
 
 void GRExprEngine::setTransferFunctions(GRTransferFuncs* tf) {
-  TF = tf;
-  TF->RegisterChecks(*this);
+  StateMgr.TF = tf;
+  getTF().RegisterChecks(*this);
 }
 
 void GRExprEngine::AddCheck(GRSimpleAPICheck* A, Stmt::StmtClass C) {
@@ -252,7 +251,7 @@ void GRExprEngine::ProcessStmt(Stmt* S, StmtNodeBuilder& builder) {
     SaveAndRestore<bool> OldPurgeDeadSymbols(Builder->PurgingDeadSymbols);
     Builder->PurgingDeadSymbols = true;
     
-    TF->EvalDeadSymbols(Tmp, *this, *Builder, EntryNode, S, 
+    getTF().EvalDeadSymbols(Tmp, *this, *Builder, EntryNode, S, 
                         CleanedState, DeadSymbols);
 
     if (!Builder->BuildSinks && !Builder->HasGeneratedNode)
@@ -964,13 +963,13 @@ void GRExprEngine::EvalStore(NodeSet& Dst, Expr* Ex, NodeTy* Pred,
 
   assert (!location.isUndef());
   
-  TF->EvalStore(Dst, *this, *Builder, Ex, Pred, St, location, Val);
+  getTF().EvalStore(Dst, *this, *Builder, Ex, Pred, St, location, Val);
   
   // Handle the case where no nodes where generated.  Auto-generate that
   // contains the updated state if we aren't generating sinks.
   
   if (!Builder->BuildSinks && Dst.size() == size && !Builder->HasGeneratedNode)
-    TF->GRTransferFuncs::EvalStore(Dst, *this, *Builder, Ex, Pred, St,
+    getTF().GRTransferFuncs::EvalStore(Dst, *this, *Builder, Ex, Pred, St,
                                    location, Val);
 }
 
@@ -1939,7 +1938,7 @@ void GRExprEngine::EvalReturn(NodeSet& Dst, ReturnStmt* S, NodeTy* Pred) {
   SaveAndRestore<bool> OldSink(Builder->BuildSinks);
   SaveOr OldHasGen(Builder->HasGeneratedNode);
 
-  TF->EvalReturn(Dst, *this, *Builder, S, Pred);
+  getTF().EvalReturn(Dst, *this, *Builder, S, Pred);
   
   // Handle the case where no nodes where generated.
   
@@ -2240,7 +2239,7 @@ void GRExprEngine::EvalBinOp(ExplodedNodeSet<ValueState>& Dst, Expr* Ex,
   unsigned size = Dst.size();
   SaveOr OldHasGen(Builder->HasGeneratedNode);
   
-  TF->EvalBinOpNN(Dst, *this, *Builder, Op, Ex, L, R, Pred);
+  getTF().EvalBinOpNN(Dst, *this, *Builder, Op, Ex, L, R, Pred);
   
   if (!Builder->BuildSinks && Dst.size() == size &&
       !Builder->HasGeneratedNode)
@@ -2248,177 +2247,6 @@ void GRExprEngine::EvalBinOp(ExplodedNodeSet<ValueState>& Dst, Expr* Ex,
 }
 
 //===----------------------------------------------------------------------===//
-// "Assume" logic.
-//===----------------------------------------------------------------------===//
-
-const ValueState* GRExprEngine::Assume(const ValueState* St, LVal Cond,
-                                       bool Assumption, bool& isFeasible) {
-                                             
-  St = AssumeAux(St, Cond, Assumption, isFeasible);
-  
-  return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
-                    : St;
-}
-
-const ValueState* GRExprEngine::AssumeAux(const ValueState* St, LVal Cond,
-                                          bool Assumption, bool& isFeasible) {
-                                       
-  switch (Cond.getSubKind()) {
-    default:
-      assert (false && "'Assume' not implemented for this LVal.");
-      return St;
-
-    case lval::SymbolValKind:
-      if (Assumption)
-        return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
-                           BasicVals.getZeroWithPtrWidth(), isFeasible);
-      else
-        return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
-                           BasicVals.getZeroWithPtrWidth(), isFeasible);
-
-
-    case lval::DeclValKind:
-    case lval::FuncValKind:
-    case lval::GotoLabelKind:
-    case lval::StringLiteralValKind:
-      isFeasible = Assumption;
-      return St;
-      
-    case lval::FieldOffsetKind:
-      return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
-                       Assumption, isFeasible);
-      
-    case lval::ArrayOffsetKind:
-      return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
-                       Assumption, isFeasible);
-      
-    case lval::ConcreteIntKind: {
-      bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
-      isFeasible = b ? Assumption : !Assumption;      
-      return St;
-    }
-  }
-}
-
-const ValueState* GRExprEngine::Assume(const ValueState* St, NonLVal Cond,
-                                       bool Assumption, bool& isFeasible) {
-
-  St = AssumeAux(St, Cond, Assumption, isFeasible);
-
-  return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
-                    : St;
-}
-
-const ValueState* GRExprEngine::AssumeAux(const ValueState* St, NonLVal Cond,
-                                          bool Assumption, bool& isFeasible) {  
-  switch (Cond.getSubKind()) {
-    default:
-      assert (false && "'Assume' not implemented for this NonLVal.");
-      return St;
-      
-      
-    case nonlval::SymbolValKind: {
-      nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
-      SymbolID sym = SV.getSymbol();
-      
-      if (Assumption)
-        return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
-                           isFeasible);
-      else
-        return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
-                           isFeasible);
-    }
-      
-    case nonlval::SymIntConstraintValKind:
-      return
-        AssumeSymInt(St, Assumption,
-                     cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
-                     isFeasible);
-      
-    case nonlval::ConcreteIntKind: {
-      bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
-      isFeasible = b ? Assumption : !Assumption;      
-      return St;
-    }
-      
-    case nonlval::LValAsIntegerKind: {
-      return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
-                       Assumption, isFeasible);
-    }
-  }
-}
-
-const ValueState* GRExprEngine::AssumeSymNE(const ValueState* St,
-                                            SymbolID sym, const llvm::APSInt& V,
-                                            bool& isFeasible) {
-  
-  // First, determine if sym == X, where X != V.
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
-    isFeasible = *X != V;
-    return St;
-  }
-  
-  // Second, determine if sym != V.
-  if (St->isNotEqual(sym, V)) {
-    isFeasible = true;
-    return St;
-  }
-      
-  // If we reach here, sym is not a constant and we don't know if it is != V.
-  // Make that assumption.
-  
-  isFeasible = true;
-  return StateMgr.AddNE(St, sym, V);
-}
-
-const ValueState* GRExprEngine::AssumeSymEQ(const ValueState* St, SymbolID sym,
-                                            const llvm::APSInt& V, bool& isFeasible) {
-  
-  // First, determine if sym == X, where X != V.
-  if (const llvm::APSInt* X = St->getSymVal(sym)) {
-    isFeasible = *X == V;
-    return St;
-  }
-  
-  // Second, determine if sym != V.
-  if (St->isNotEqual(sym, V)) {
-    isFeasible = false;
-    return St;
-  }
-  
-  // If we reach here, sym is not a constant and we don't know if it is == V.
-  // Make that assumption.
-  
-  isFeasible = true;
-  return StateMgr.AddEQ(St, sym, V);
-}
-
-const ValueState* GRExprEngine::AssumeSymInt(const ValueState* St,
-                                             bool Assumption,
-                                             const SymIntConstraint& C,
-                                             bool& isFeasible) {
-  
-  switch (C.getOpcode()) {
-    default:
-      // No logic yet for other operators.
-      isFeasible = true;
-      return St;
-      
-    case BinaryOperator::EQ:
-      if (Assumption)
-        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
-      else
-        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
-      
-    case BinaryOperator::NE:
-      if (Assumption)
-        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
-      else
-        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
-  }
-}
-
-//===----------------------------------------------------------------------===//
 // Visualization.
 //===----------------------------------------------------------------------===//
 
@@ -2733,7 +2561,7 @@ void GRExprEngine::ViewGraph(bool trim) {
   else {
     GraphPrintCheckerState = this;
     GraphPrintSourceManager = &getContext().getSourceManager();
-    GraphCheckerStatePrinter = TF->getCheckerStatePrinter();
+    GraphCheckerStatePrinter = getTF().getCheckerStatePrinter();
 
     llvm::ViewGraph(*G.roots_begin(), "GRExprEngine");
     
@@ -2748,7 +2576,7 @@ void GRExprEngine::ViewGraph(NodeTy** Beg, NodeTy** End) {
 #ifndef NDEBUG
   GraphPrintCheckerState = this;
   GraphPrintSourceManager = &getContext().getSourceManager();
-  GraphCheckerStatePrinter = TF->getCheckerStatePrinter();
+  GraphCheckerStatePrinter = getTF().getCheckerStatePrinter();
   
   GRExprEngine::GraphTy* TrimmedG = G.Trim(Beg, End);
 
diff --git a/lib/Analysis/ValueState.cpp b/lib/Analysis/ValueState.cpp
index ca78faf349..2c3e6dabc6 100644
--- a/lib/Analysis/ValueState.cpp
+++ b/lib/Analysis/ValueState.cpp
@@ -13,6 +13,7 @@
 
 #include "clang/Analysis/PathSensitive/ValueState.h"
 #include "llvm/ADT/SmallSet.h"
+#include "clang/Analysis/PathSensitive/GRTransferFuncs.h"
 
 using namespace clang;
 
@@ -294,3 +295,174 @@ void ValueState::print(std::ostream& Out, CheckerStatePrinter* P,
   if (P && CheckerState)
     P->PrintCheckerState(Out, CheckerState, nl, sep);
 }
+
+//===----------------------------------------------------------------------===//
+// "Assume" logic.
+//===----------------------------------------------------------------------===//
+
+const ValueState* ValueStateManager::Assume(const ValueState* St, LVal Cond,
+                                            bool Assumption, bool& isFeasible) {
+  
+  St = AssumeAux(St, Cond, Assumption, isFeasible);
+  
+  return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
+                    : St;
+}
+
+const ValueState* ValueStateManager::AssumeAux(const ValueState* St, LVal Cond,
+                                          bool Assumption, bool& isFeasible) {
+  
+  switch (Cond.getSubKind()) {
+    default:
+      assert (false && "'Assume' not implemented for this LVal.");
+      return St;
+      
+    case lval::SymbolValKind:
+      if (Assumption)
+        return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+                           BasicVals.getZeroWithPtrWidth(), isFeasible);
+      else
+        return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+                           BasicVals.getZeroWithPtrWidth(), isFeasible);
+      
+      
+    case lval::DeclValKind:
+    case lval::FuncValKind:
+    case lval::GotoLabelKind:
+    case lval::StringLiteralValKind:
+      isFeasible = Assumption;
+      return St;
+      
+    case lval::FieldOffsetKind:
+      return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
+                       Assumption, isFeasible);
+      
+    case lval::ArrayOffsetKind:
+      return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
+                       Assumption, isFeasible);
+      
+    case lval::ConcreteIntKind: {
+      bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
+      isFeasible = b ? Assumption : !Assumption;      
+      return St;
+    }
+  }
+}
+
+const ValueState* ValueStateManager::Assume(const ValueState* St, NonLVal Cond,
+                                       bool Assumption, bool& isFeasible) {
+  
+  St = AssumeAux(St, Cond, Assumption, isFeasible);
+  
+  return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
+  : St;
+}
+
+const ValueState* ValueStateManager::AssumeAux(const ValueState* St, NonLVal Cond,
+                                          bool Assumption, bool& isFeasible) {  
+  switch (Cond.getSubKind()) {
+    default:
+      assert (false && "'Assume' not implemented for this NonLVal.");
+      return St;
+      
+      
+    case nonlval::SymbolValKind: {
+      nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
+      SymbolID sym = SV.getSymbol();
+      
+      if (Assumption)
+        return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
+                           isFeasible);
+      else
+        return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
+                           isFeasible);
+    }
+      
+    case nonlval::SymIntConstraintValKind:
+      return
+      AssumeSymInt(St, Assumption,
+                   cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
+                   isFeasible);
+      
+    case nonlval::ConcreteIntKind: {
+      bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
+      isFeasible = b ? Assumption : !Assumption;      
+      return St;
+    }
+      
+    case nonlval::LValAsIntegerKind: {
+      return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
+                       Assumption, isFeasible);
+    }
+  }
+}
+
+const ValueState* ValueStateManager::AssumeSymNE(const ValueState* St,
+                                            SymbolID sym, const llvm::APSInt& V,
+                                            bool& isFeasible) {
+  
+  // First, determine if sym == X, where X != V.
+  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+    isFeasible = *X != V;
+    return St;
+  }
+  
+  // Second, determine if sym != V.
+  if (St->isNotEqual(sym, V)) {
+    isFeasible = true;
+    return St;
+  }
+  
+  // If we reach here, sym is not a constant and we don't know if it is != V.
+  // Make that assumption.
+  
+  isFeasible = true;
+  return AddNE(St, sym, V);
+}
+
+const ValueState* ValueStateManager::AssumeSymEQ(const ValueState* St, SymbolID sym,
+                                            const llvm::APSInt& V, bool& isFeasible) {
+  
+  // First, determine if sym == X, where X != V.
+  if (const llvm::APSInt* X = St->getSymVal(sym)) {
+    isFeasible = *X == V;
+    return St;
+  }
+  
+  // Second, determine if sym != V.
+  if (St->isNotEqual(sym, V)) {
+    isFeasible = false;
+    return St;
+  }
+  
+  // If we reach here, sym is not a constant and we don't know if it is == V.
+  // Make that assumption.
+  
+  isFeasible = true;
+  return AddEQ(St, sym, V);
+}
+
+const ValueState* ValueStateManager::AssumeSymInt(const ValueState* St,
+                                             bool Assumption,
+                                             const SymIntConstraint& C,
+                                             bool& isFeasible) {
+  
+  switch (C.getOpcode()) {
+    default:
+      // No logic yet for other operators.
+      isFeasible = true;
+      return St;
+      
+    case BinaryOperator::EQ:
+      if (Assumption)
+        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
+      else
+        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
+      
+    case BinaryOperator::NE:
+      if (Assumption)
+        return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
+      else
+        return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
+  }
+}