Kill off UpdateList::isRooted flag.

 - The right way to handle this is by using constant arrays, where the semantics
   are easier to define and implement.


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

1 files changed, 5 insertions, 5 deletions

diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index ea5427e3..1d06ca33 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -352,7 +352,7 @@ protected:
     // If the index is out of range, we cannot assign it a value, since that
     // value cannot be part of the assignment.
     if (index >= array.size)
-      return ReadExpr::create(UpdateList(&array, true, 0), 
+      return ReadExpr::create(UpdateList(&array, 0), 
                               ConstantExpr::alloc(index, Expr::Int32));
       
     std::map<unsigned, CexObjectData*>::iterator it = objects.find(array.id);
@@ -373,17 +373,17 @@ protected:
     // If the index is out of range, we cannot assign it a value, since that
     // value cannot be part of the assignment.
     if (index >= array.size)
-      return ReadExpr::create(UpdateList(&array, true, 0), 
+      return ReadExpr::create(UpdateList(&array, 0), 
                               ConstantExpr::alloc(index, Expr::Int32));
       
     std::map<unsigned, CexObjectData*>::iterator it = objects.find(array.id);
     if (it == objects.end())
-      return ReadExpr::create(UpdateList(&array, true, 0), 
+      return ReadExpr::create(UpdateList(&array, 0), 
                               ConstantExpr::alloc(index, Expr::Int32));
 
     CexValueData cvd = it->second->getExactValues(index);
     if (!cvd.isFixed())
-      return ReadExpr::create(UpdateList(&array, true, 0), 
+      return ReadExpr::create(UpdateList(&array, 0), 
                               ConstantExpr::alloc(index, Expr::Int32));
 
     return ConstantExpr::alloc(cvd.min(), Expr::Int8);
@@ -1020,7 +1020,7 @@ FastCexSolver::computeInitialValues(const Query& query,
 
     for (unsigned i=0; i < array->size; i++) {
       ref<Expr> read = 
-        ReadExpr::create(UpdateList(array, true, 0),
+        ReadExpr::create(UpdateList(array, 0),
                          ConstantExpr::create(i, kMachinePointerType));
       ref<Expr> value = cd.evaluatePossible(read);