Nice patch by Hristina Palikareva that removes the dependency on STP

arrays from the Array and UpdateNode classes.



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

2 files changed, 8 insertions, 10 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 089e78b3..fa8525b6 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -488,11 +488,13 @@ ref<Expr>  NotOptimizedExpr::create(ref<Expr> src) {
 extern "C" void vc_DeleteExpr(void*);
 
 Array::~Array() {
-  // FIXME: This shouldn't be necessary.
-  if (stpInitialArray) {
-    ::vc_DeleteExpr(stpInitialArray);
-    stpInitialArray = 0;
-  }
+}
+
+unsigned Array::computeHash() {
+  unsigned res = 0;
+  for (unsigned i = 0, e = name.size(); i != e; ++i)
+    res = (res * Expr::MAGIC_HASH_CONSTANT) + name[i];
+  return res; 
 }
 
 /***/
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 379f1c8d..14fd8308 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -18,8 +18,7 @@ using namespace klee;
 UpdateNode::UpdateNode(const UpdateNode *_next, 
                        const ref<Expr> &_index, 
                        const ref<Expr> &_value) 
-  : refCount(0),
-    stpArray(0),
+  : refCount(0),    
     next(_next),
     index(_index),
     value(_value) {
@@ -36,9 +35,6 @@ UpdateNode::UpdateNode(const UpdateNode *_next,
 extern "C" void vc_DeleteExpr(void*);
 
 UpdateNode::~UpdateNode() {
-  // XXX gross
-  if (stpArray)
-    ::vc_DeleteExpr(stpArray);
 }
 
 int UpdateNode::compare(const UpdateNode &b) const {