some more tests for the context.

2 files changed, 98 insertions, 5 deletions

diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index 44ed52dea..eef2317ea 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -1,8 +1,6 @@
 /*********************                                           -*- C++ -*-  */
-/** node_black.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
+/** context_black.h
+ ** Original author: dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -17,6 +15,7 @@
 
 //Used in some of the tests
 #include <vector>
+#include <iostream>
 #include "context/context.h"
 
 using namespace std;
@@ -34,10 +33,29 @@ public:
   }
 
   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 tearDown(){
+  void testContextPushPop() {
+    // Test what happens when the context is popped below 0
+    // the interface doesn't declare any exceptions
+    d_context->push();
+    d_context->pop();
+    d_context->pop();
+    d_context->pop();
+  }
+
+  void tearDown() {
     delete d_context;
   }
 };
diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h
new file mode 100644
index 000000000..534f490f6
--- /dev/null
+++ b/test/unit/context/context_mm_black.h
@@ -0,0 +1,75 @@
+/*********************                                           -*- C++ -*-  */
+/** context_mm_black.h
+ ** Original author: dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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::Node.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <cstring>
+
+//Used in some of the tests
+#include <vector>
+#include <iostream>
+#include "context/context_mm.h"
+
+using namespace std;
+using namespace CVC4::context;
+
+class ContextBlack : public CxxTest::TestSuite {
+private:
+
+  ContextMemoryManager* d_cmm;
+
+public:
+
+  void setUp() {
+    d_cmm = new ContextMemoryManager();
+  }
+
+  void testPushPop() {
+
+    // Push, then allocate, then pop
+    for (int p = 0; p < 5; ++ p) {
+      d_cmm->push();
+      for (int i = 1; i < 16384/3; ++i) {
+        int len = i*3;
+        char* newMem = (char*)d_cmm->newData(len);
+        for(int k = 0; k < len - 1; k ++)
+          newMem[k] = 'a';
+        newMem[len-1] = 0;
+        TS_ASSERT(strlen(newMem) == len - 1);
+      }
+      d_cmm->pop();
+    }
+
+    // Push, then allocate, then pop all at once
+    for (int p = 0; p < 5; ++ p) {
+      d_cmm->push();
+      for (int i = 1; i < 16384/3; ++i) {
+        int len = i*3;
+        char* newMem = (char*)d_cmm->newData(len);
+        for(int k = 0; k < len - 1; k ++)
+          newMem[k] = 'a';
+        newMem[len-1] = 0;
+        TS_ASSERT(strlen(newMem) == len - 1);
+      }
+    }
+    for (int p = 0; p < 5; ++ p) {
+      d_cmm->pop();
+    }
+
+    // Try poping out of scope
+    d_cmm->pop();
+  }
+
+  void tearDown() {
+    delete d_cmm;
+  }
+};