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

2 files changed, 3 insertions, 5 deletions

diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 8f144456..ba1b8e1f 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -102,7 +102,7 @@ ObjectState::ObjectState(const MemoryObject *mo, unsigned _size)
     flushMask(0),
     knownSymbolics(0),
     size(_size),
-    updates(mo->array, false, 0),
+    updates(mo->array, 0),
     readOnly(false) {
 }
 
@@ -149,7 +149,6 @@ void ObjectState::makeConcrete() {
 void ObjectState::makeSymbolic() {
   assert(!updates.head &&
          "XXX makeSymbolic of objects with symbolic values is unsupported");
-  updates.isRooted = true;
 
   // XXX simplify this, can just delete various arrays I guess
   for (unsigned i=0; i<size; i++) {
@@ -792,7 +791,6 @@ void ObjectState::print() {
   llvm::cerr << "-- ObjectState --\n";
   llvm::cerr << "\tMemoryObject ID: " << object->id << "\n";
   llvm::cerr << "\tRoot Object: " << updates.root << "\n";
-  llvm::cerr << "\tIs Rooted? " << updates.isRooted << "\n";
   llvm::cerr << "\tSize: " << size << "\n";
 
   llvm::cerr << "\tBytes:\n";
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 6fcfe596..dc3ff931 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -87,7 +87,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
          it = directReads.begin(), ie = directReads.end(); it != ie; ++it) {
     const Array *array = it->first;
     unsigned i = it->second;
-    ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
+    ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
                                       ConstantExpr::alloc(i, Expr::Int32));
     
     // If not in bindings then this can't be a violation?
@@ -124,7 +124,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
          ie = assignment.bindings.end(); it != ie; ++it) {
     const Array *array = it->first;
     for (unsigned i=0; i<array->size; ++i) {
-      ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
+      ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
                                         ConstantExpr::alloc(i, Expr::Int32));
       ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8));
       bool res;