From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 2 Feb 2010 22:01:59 +0000 (+0000)
Subject: beginings of test for CDO. one fail
X-Git-Tag: cvc5-1.0.0~9312
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ad9aa3d20a8938e2dc9fbd6a6ddd85d1b417eb21;p=cvc5.git

beginings of test for CDO. one fail
---

diff --git a/src/context/context.h b/src/context/context.h
index c59955f8d..2a4b2df2f 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -314,13 +314,6 @@ class ContextObj {
    */
   ContextObj* restoreAndContinue();
 
-  /**
-   * Disable delete: objects allocated with new(ContextMemorymanager) should
-   * never be deleted.  Objects allocated with new(bool) should be deleted by
-   * calling deleteSelf().
-   */
-  static void operator delete(void* pMem) { }
-
 protected:
   /**
    * This is a method that must be implemented by all classes inheriting from
@@ -398,6 +391,15 @@ public:
    */
   void deleteSelf() { ::operator delete(this); }
 
+  /**
+   * Disable delete: objects allocated with new(ContextMemorymanager) should
+   * never be deleted.  Objects allocated with new(bool) should be deleted by
+   * calling deleteSelf().
+   */
+  static void operator delete(void* pMem) {
+    AlwaysAssert(false, "Not Allowed!");
+  }
+
 }; /* class ContextObj */
 
   /**
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index dfe345afe..9984a9111 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -2,7 +2,8 @@
 UNIT_TESTS = \
 	expr/node_white \
 	expr/node_black \
-	parser/parser_black
+	parser/parser_black \
+	context/context_black
 
 # Things that aren't tests but that tests rely on and need to
 # go into the distribution
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
new file mode 100644
index 000000000..44ed52dea
--- /dev/null
+++ b/test/unit/context/context_black.h
@@ -0,0 +1,43 @@
+/*********************                                           -*- C++ -*-  */
+/** node_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): 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>
+
+//Used in some of the tests
+#include <vector>
+#include "context/context.h"
+
+using namespace std;
+using namespace CVC4::context;
+
+class ContextBlack : public CxxTest::TestSuite {
+private:
+
+  Context* d_context;
+
+public:
+
+  void setUp() {
+    d_context = new Context();
+  }
+
+  void testIntCDO() {
+    CDO<int> a1(d_context);
+  }
+
+  void tearDown(){
+    delete d_context;
+  }
+};