I think this finishes off the CDMap<>/Attribute leaks

4 files changed, 461 insertions, 18 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 214f2ac58..122d92cae 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -10,15 +10,17 @@ UNIT_TESTS = \
 	parser/parser_black \
 	context/context_black \
 	context/context_mm_black \
+	context/cdo_black \
 	context/cdlist_black \
+	context/cdmap_black \
 	theory/theory_black \
 	theory/theory_uf_white \
 	util/assert_white \
 	util/configuration_white \
-	util/output_white \
-	util/integer_black \
-	util/integer_white \
-	util/rational_white
+	util/output_white
+#	util/integer_black \
+#	util/integer_white \
+#	util/rational_white
 
 # Things that aren't tests but that tests rely on and need to
 # go into the distribution
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
new file mode 100644
index 000000000..7040e4cc1
--- /dev/null
+++ b/test/unit/context/cdmap_black.h
@@ -0,0 +1,398 @@
+/*********************                                                        */
+/** cdmap_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::context::CDMap<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/cdmap.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class CDMapBlack : public CxxTest::TestSuite {
+
+  Context* d_context;
+
+public:
+
+  void setUp() {
+    d_context = new Context;
+    //Debug.on("cdmap");
+  }
+
+  void tearDown() {
+    delete d_context;
+  }
+
+  void testSimpleSequence() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+
+          map.insert(1, 45);
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      d_context->pop();
+    }
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+  }
+
+  // no intervening find() in this one
+  // (under the theory that this could trigger a bug)
+  void testSimpleSequenceFewerFinds() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    {
+      d_context->push();
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      {
+        d_context->push();
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(7) == map.end());
+
+        {
+          d_context->push();
+
+          d_context->pop();
+        }
+
+        d_context->pop();
+      }
+
+      d_context->pop();
+    }
+  }
+
+  void testObliterate() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        map.obliterate(5);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) == map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) == map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) == map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      d_context->pop();
+    }
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+  }
+
+  void testObliteratePrimordial() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        map.obliterate(3);
+
+        TS_ASSERT(map.find(3) == map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) == map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) == map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) == map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      d_context->pop();
+    }
+
+    TS_ASSERT(map.find(3) == map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+  }
+
+  void testObliterateCurrent() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        map.obliterate(1);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) == map.end());
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      d_context->pop();
+    }
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+  }
+};
diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h
new file mode 100644
index 000000000..4cdb8f343
--- /dev/null
+++ b/test/unit/context/cdo_black.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/** cdo_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::context::CDO<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <vector>
+#include <iostream>
+#include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class CDOBlack : public CxxTest::TestSuite {
+private:
+
+  Context* d_context;
+
+public:
+
+  void setUp() {
+    d_context = new Context;
+  }
+
+  void tearDown() {
+    delete d_context;
+  }
+
+  void testIntCDO() {
+    // Test that push/pop maintains the original value
+    CDO<int> a1(d_context);
+    a1 = 5;
+    TS_ASSERT(d_context->getLevel() == 0);
+    d_context->push();
+    a1 = 10;
+    TS_ASSERT(d_context->getLevel() == 1);
+    TS_ASSERT(a1 == 10);
+    d_context->pop();
+    TS_ASSERT(d_context->getLevel() == 0);
+    TS_ASSERT(a1 == 5);
+  }
+};
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index c9b47e400..338c09849 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -41,20 +41,6 @@ public:
     delete d_context;
   }
 
-  void testIntCDO() {
-    // Test that push/pop maintains the original value
-    CDO<int> a1(d_context);
-    a1 = 5;
-    TS_ASSERT(d_context->getLevel() == 0);
-    d_context->push();
-    a1 = 10;
-    TS_ASSERT(d_context->getLevel() == 1);
-    TS_ASSERT(a1 == 10);
-    d_context->pop();
-    TS_ASSERT(d_context->getLevel() == 0);
-    TS_ASSERT(a1 == 5);
-  }
-
   void testContextPushPop() {
     // Test what happens when the context is popped below 0
     // the interface doesn't declare any exceptions