From: Dejan Jovanović 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 + +//Used in some of the tests +#include +#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 a1(d_context); + } + + void tearDown(){ + delete d_context; + } +};