From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 13 Mar 2010 01:57:01 +0000 (+0000)
Subject: Fix for bug 45
X-Git-Tag: cvc5-1.0.0~9178
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7eff5dfa38e016bb759a5daf5b0afef0a057eb47;p=cvc5.git

Fix for bug 45
---

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index fd50d4149..e3c7e155c 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -138,15 +138,9 @@ public:
    * Destructor: delete the list
    */
   ~CDList() throw(AssertionException) {
-    if(d_list != NULL) {
-      if(d_callDestructor) {
-        while(d_size != 0) {
-          --d_size;
-          d_list[d_size].~T();
-        }
-      }
-      free(d_list);
-    }
+    T* list = d_list;
+    destroy();
+    free(list);
   }
 
   /**
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index b1bb47c4c..460f917ff 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -101,7 +101,7 @@ public:
     }
   }
 
-  ~CDOmap() throw(AssertionException) {}
+  ~CDOmap() throw(AssertionException) { destroy(); }
 
   void set(const Data& data) {
     makeCurrent();
diff --git a/src/context/cdo.h b/src/context/cdo.h
index aca48d264..f2d6e7b4b 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -84,9 +84,9 @@ public:
   }
 
   /**
-   * Destructor - no need to do anything.
+   * Destructor - call destroy() method
    */
-  ~CDO() throw() {}
+  ~CDO() throw() { destroy(); }
 
   /**
    * Set the data in the CDO.  First call makeCurrent.
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 8e87741b5..d2e2bfa1b 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -175,17 +175,7 @@ ContextObj* ContextObj::restoreAndContinue() {
 }
 
 
-ContextObj::ContextObj(Context* pContext) :
-  d_pContextObjRestore(NULL) {
-
-  Assert(pContext != NULL, "NULL context pointer");
-
-  d_pScope = pContext->getBottomScope();
-  d_pScope->addToChain(this);
-}
-
-
-ContextObj::~ContextObj() throw(AssertionException) {
+void ContextObj::destroy() throw(AssertionException) {
   for(;;) {
     if(next() != NULL) {
       next()->prev() = prev();
@@ -199,6 +189,16 @@ ContextObj::~ContextObj() throw(AssertionException) {
 }
 
 
+ContextObj::ContextObj(Context* pContext) :
+  d_pContextObjRestore(NULL) {
+
+  Assert(pContext != NULL, "NULL context pointer");
+
+  d_pScope = pContext->getBottomScope();
+  d_pScope->addToChain(this);
+}
+
+
 ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
   if(preNotify) {
     pContext->addNotifyObjPre(this);
diff --git a/src/context/context.h b/src/context/context.h
index 69e8fe776..6b9f9fd6d 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -273,6 +273,10 @@ public:
  *    ContextMemoryManager (see item 2 above).
  * 4. In the subclass implementation, any time the state is about to be
  *    changed, first call makeCurrent().
+ * 5. In the subclass implementation, the destructor should call destroy().
+ *    Unfortunately, the destroy() functionality cannot be in the ContextObj
+ *    destructor since it needs to call the subclass-specific restore() method
+ *    in order to properly clean up saved copies.
  */
 class ContextObj {
   /**
@@ -352,6 +356,14 @@ protected:
     }
   }
 
+  /**
+   * Should be called from sub-class destructor: calls restore until restored
+   * to initial version.  Also removes object from all Scope lists.  Note that
+   * this doesn't actually free the memory allocated by the ContextMemoryManager
+   * for this object.  This isn't done until the corresponding Scope is popped.
+   */
+  void destroy() throw(AssertionException);
+
   /**
    * operator new using ContextMemoryManager (common case used by
    * subclasses during save() ).  No delete is required for memory
@@ -385,13 +397,9 @@ public:
   ContextObj(Context* context);
 
   /**
-   * Destructor: Calls restore until restored to initial version.
-   * Also removes object from all Scope lists.  Note that this doesn't
-   * actually free the memory allocated by the ContextMemoryManager
-   * for this object.  This isn't done until the corresponding Scope
-   * is popped.
+   * Destructor does nothing: subclass must explicitly call destroy() instead.
    */
-  virtual ~ContextObj() throw(AssertionException);
+  virtual ~ContextObj() {}
 
   /**
    * If you want to allocate a ContextObj object on the heap, use this