diff options
Diffstat (limited to 'test/unit/context/context_black.h')
-rw-r--r-- | test/unit/context/context_black.h | 28 |
1 files changed, 23 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; } }; |