Move Array construction out of MemoryObject into ObjectState.

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

4 files changed, 15 insertions, 18 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 9afbabd7..878a70ba 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -507,10 +507,7 @@ public:
              "Invalid initial constant value!");
 #endif
   }
-  ~Array() {
-    // FIXME: This relies on caller to delete the STP array.
-    assert(!stpInitialArray && "Array must be deleted by caller!");
-  }
+  ~Array();
 
   bool isSymbolicArray() const { return constantValues.empty(); }
   bool isConstantArray() const { return !isSymbolicArray(); }
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index ba1b8e1f..513c2177 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -57,16 +57,6 @@ int MemoryObject::counter = 0;
 extern "C" void vc_DeleteExpr(void*);
 
 MemoryObject::~MemoryObject() {
-  // FIXME: This shouldn't be necessary. Array's should be ref-counted
-  // just like everything else, and the interaction with the STP array
-  // should hide at least inside the Expr/Solver layers.
-  if (array) {
-    if (array->stpInitialArray) {
-      ::vc_DeleteExpr(array->stpInitialArray);
-      array->stpInitialArray = 0;
-    }
-    delete array;
-  }
 }
 
 void MemoryObject::getAllocInfo(std::string &result) const {
@@ -102,7 +92,8 @@ ObjectState::ObjectState(const MemoryObject *mo, unsigned _size)
     flushMask(0),
     knownSymbolics(0),
     size(_size),
-    updates(mo->array, 0),
+    // FIXME: Leaked!
+    updates(new Array("arr" + llvm::utostr(mo->id), _size), 0),
     readOnly(false) {
 }
 
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index b6ea81d7..565572be 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -36,7 +36,6 @@ private:
 public:
   unsigned id;
   uint64_t address;
-  Array *array;
 
   /// size in bytes
   unsigned size;
@@ -71,7 +70,6 @@ public:
   MemoryObject(uint64_t _address) 
     : id(counter++),
       address(_address),
-      array(new Array("arr" + llvm::utostr(id), id)),
       size(0),
       isFixed(true),
       allocSite(0) {
@@ -82,7 +80,6 @@ public:
                const llvm::Value *_allocSite) 
     : id(counter++),
       address(_address),
-      array(new Array("arr" + llvm::utostr(id), _size)),
       size(_size),
       name("unnamed"),
       isLocal(_isLocal),
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 2b6f3d96..ce914266 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -353,6 +353,18 @@ ref<Expr>  NotOptimizedExpr::create(ref<Expr> src) {
   return NotOptimizedExpr::alloc(src);
 }
 
+/***/
+
+Array::~Array() {
+  // FIXME: This shouldn't be necessary.
+  if (array->stpInitialArray) {
+    ::vc_DeleteExpr(array->stpInitialArray);
+    array->stpInitialArray = 0;
+  }
+}
+
+/***/
+
 ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
   // rollback index when possible...