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, 2 insertions, 5 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index d1fdfa73..e774eaff 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -507,11 +507,8 @@ public:
   /// pointer to the most recent update node
   const UpdateNode *head;
   
-  // shouldn't this be part of the ReadExpr? 
-  bool isRooted;
-
 public:
-  UpdateList(const Array *_root, bool isRooted, const UpdateNode *_head);
+  UpdateList(const Array *_root, const UpdateNode *_head);
   UpdateList(const UpdateList &b);
   ~UpdateList();
   
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 051a84f9..458b8d8d 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -72,7 +72,7 @@ namespace klee {
       return ConstantExpr::alloc(it->second[index], Expr::Int8);
     } else {
       if (allowFreeValues) {
-        return ReadExpr::create(UpdateList(array, true, 0), 
+        return ReadExpr::create(UpdateList(array, 0), 
                                 ConstantExpr::alloc(index, Expr::Int32));
       } else {
         return ConstantExpr::alloc(0, Expr::Int8);