--- /dev/null
+/********************* */
+/*! \file context_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::context::Context.
+ **
+ ** Black box testing of CVC4::context::Context.
+ **/
+
+#include <iostream>
+#include <vector>
+
+#include "base/exception.h"
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "test_context.h"
+
+namespace CVC4 {
+
+using namespace context;
+
+namespace test {
+
+struct MyContextNotifyObj : public ContextNotifyObj
+{
+ int32_t d_ncalls;
+
+ MyContextNotifyObj(Context* context, bool pre)
+ : ContextNotifyObj(context, pre), d_ncalls(0)
+ {
+ }
+
+ ~MyContextNotifyObj() override {}
+
+ void contextNotifyPop() override { ++d_ncalls; }
+};
+
+class MyContextObj : public ContextObj
+{
+ MyContextNotifyObj& notify;
+
+ public:
+ MyContextObj(Context* context, MyContextNotifyObj& n)
+ : ContextObj(context), notify(n), d_ncalls(0), d_nsaves(0)
+ {
+ }
+
+ MyContextObj(bool topScope, Context* context, MyContextNotifyObj& n)
+ : ContextObj(topScope, context), notify(n), d_ncalls(0), d_nsaves(0)
+ {
+ }
+
+ ~MyContextObj() override { destroy(); }
+
+ ContextObj* save(ContextMemoryManager* pcmm) override
+ {
+ ++d_nsaves;
+ return new (pcmm) MyContextObj(*this);
+ }
+
+ void restore(ContextObj* contextObj) override { d_ncalls = notify.d_ncalls; }
+
+ void makeCurrent() { ContextObj::makeCurrent(); }
+
+ int d_ncalls;
+ int d_nsaves;
+
+ private:
+ MyContextObj(const MyContextObj& other)
+ : ContextObj(other), notify(other.notify), d_ncalls(0), d_nsaves(0)
+ {
+ }
+};
+
+class TestContextBlack : public TestContext
+{
+};
+
+TEST_F(TestContextBlack, push_pop)
+{
+ // Test what happens when the context is popped below 0
+ // the interface doesn't declare any exceptions
+ d_context->push();
+ d_context->pop();
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
+ ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
+#endif /* CVC4_ASSERTIONS */
+}
+
+TEST_F(TestContextBlack, dtor)
+{
+ // Destruction of ContextObj was broken in revision 324 (bug #45) when
+ // at a higher context level with an intervening modification.
+ // (The following caused a "pure virtual method called" error.)
+ CDO<int> i(d_context.get());
+ d_context->push();
+ i = 5;
+}
+
+TEST_F(TestContextBlack, pre_post_notify)
+{
+ // This is tricky; we want to detect if pre- and post-notifies are
+ // done correctly. For that, we have to use a special ContextObj,
+ // since that's the only thing that runs between pre- and post-.
+
+ MyContextNotifyObj a(d_context.get(), true), b(d_context.get(), false);
+
+ try
+ {
+ MyContextNotifyObj c(d_context.get(), true), d(d_context.get(), false);
+
+ EXPECT_EQ(a.d_ncalls, 0);
+ EXPECT_EQ(b.d_ncalls, 0);
+ EXPECT_EQ(c.d_ncalls, 0);
+ EXPECT_EQ(d.d_ncalls, 0);
+
+ MyContextObj w(d_context.get(), a);
+ MyContextObj x(d_context.get(), b);
+ MyContextObj y(d_context.get(), c);
+ MyContextObj z(d_context.get(), d);
+
+ d_context->push();
+
+ w.makeCurrent();
+ x.makeCurrent();
+ y.makeCurrent();
+ z.makeCurrent();
+
+ EXPECT_EQ(a.d_ncalls, 0);
+ EXPECT_EQ(b.d_ncalls, 0);
+ EXPECT_EQ(c.d_ncalls, 0);
+ EXPECT_EQ(d.d_ncalls, 0);
+
+ EXPECT_EQ(w.d_ncalls, 0);
+ EXPECT_EQ(x.d_ncalls, 0);
+ EXPECT_EQ(y.d_ncalls, 0);
+ EXPECT_EQ(z.d_ncalls, 0);
+
+ d_context->push();
+
+ w.makeCurrent();
+ x.makeCurrent();
+ y.makeCurrent();
+ z.makeCurrent();
+
+ EXPECT_EQ(a.d_ncalls, 0);
+ EXPECT_EQ(b.d_ncalls, 0);
+ EXPECT_EQ(c.d_ncalls, 0);
+ EXPECT_EQ(d.d_ncalls, 0);
+
+ EXPECT_EQ(w.d_ncalls, 0);
+ EXPECT_EQ(x.d_ncalls, 0);
+ EXPECT_EQ(y.d_ncalls, 0);
+ EXPECT_EQ(z.d_ncalls, 0);
+
+ d_context->pop();
+
+ EXPECT_EQ(a.d_ncalls, 1);
+ EXPECT_EQ(b.d_ncalls, 1);
+ EXPECT_EQ(c.d_ncalls, 1);
+ EXPECT_EQ(d.d_ncalls, 1);
+
+ EXPECT_EQ(w.d_ncalls, 1);
+ EXPECT_EQ(x.d_ncalls, 0);
+ EXPECT_EQ(y.d_ncalls, 1);
+ EXPECT_EQ(z.d_ncalls, 0);
+
+ d_context->pop();
+
+ EXPECT_EQ(a.d_ncalls, 2);
+ EXPECT_EQ(b.d_ncalls, 2);
+ EXPECT_EQ(c.d_ncalls, 2);
+ EXPECT_EQ(d.d_ncalls, 2);
+
+ EXPECT_EQ(w.d_ncalls, 2);
+ EXPECT_EQ(x.d_ncalls, 1);
+ EXPECT_EQ(y.d_ncalls, 2);
+ EXPECT_EQ(z.d_ncalls, 1);
+ }
+ catch (Exception& e)
+ {
+ std::cerr << e.toString() << std::endl;
+ ASSERT_TRUE(false) << "Exception thrown from test";
+ }
+
+ // we do this (together with the { } block above) to get full code
+ // coverage of destruction paths; a and b haven't been destructed
+ // yet, here.
+ d_context.reset(nullptr);
+}
+
+TEST_F(TestContextBlack, top_scope_context_obj)
+{
+ // this test's implementation is based on the fact that a
+ // ContextObj allocated primordially "in the top scope" (first arg
+ // to ctor is "true"), doesn't get updated if you immediately call
+ // makeCurrent().
+
+ MyContextNotifyObj n(d_context.get(), true);
+
+ d_context->push();
+
+ MyContextObj x(true, d_context.get(), n);
+ MyContextObj y(false, d_context.get(), n);
+
+ EXPECT_EQ(x.d_nsaves, 0);
+ EXPECT_EQ(y.d_nsaves, 0);
+
+ x.makeCurrent();
+ y.makeCurrent();
+
+ EXPECT_EQ(x.d_nsaves, 0);
+ EXPECT_EQ(y.d_nsaves, 1);
+
+ d_context->push();
+
+ x.makeCurrent();
+ y.makeCurrent();
+
+ EXPECT_EQ(x.d_nsaves, 1);
+ EXPECT_EQ(y.d_nsaves, 2);
+
+ d_context->pop();
+ d_context->pop();
+
+ EXPECT_EQ(x.d_nsaves, 1);
+ EXPECT_EQ(y.d_nsaves, 2);
+}
+
+} // namespace test
+} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file context_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::context::Context.
- **
- ** Black box testing of CVC4::context::Context.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <vector>
-
-#include "base/exception.h"
-#include "context/cdlist.h"
-#include "context/cdo.h"
-#include "context/context.h"
-#include "test_utils.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::context;
-
-struct MyContextNotifyObj : public ContextNotifyObj {
- int nCalls;
-
- MyContextNotifyObj(Context* context, bool pre) :
- ContextNotifyObj(context, pre),
- nCalls(0) {
- }
-
- ~MyContextNotifyObj() override {}
-
- void contextNotifyPop() override { ++nCalls; }
-};
-
-class MyContextObj : public ContextObj {
- MyContextNotifyObj& notify;
-
-public:
- int nCalls;
- int nSaves;
-
-private:
- MyContextObj(const MyContextObj& other) :
- ContextObj(other),
- notify(other.notify),
- nCalls(0),
- nSaves(0) {
- }
-
-public:
-
- MyContextObj(Context* context, MyContextNotifyObj& n) :
- ContextObj(context),
- notify(n),
- nCalls(0),
- nSaves(0) {
- }
-
- MyContextObj(bool topScope, Context* context, MyContextNotifyObj& n) :
- ContextObj(topScope, context),
- notify(n),
- nCalls(0),
- nSaves(0) {
- }
-
- ~MyContextObj() override { destroy(); }
-
- ContextObj* save(ContextMemoryManager* pcmm) override
- {
- ++nSaves;
- return new(pcmm) MyContextObj(*this);
- }
-
- void restore(ContextObj* contextObj) override { nCalls = notify.nCalls; }
-
- void makeCurrent() {
- ContextObj::makeCurrent();
- }
-};
-
-
-class ContextBlack : public CxxTest::TestSuite {
-private:
-
- Context* d_context;
-
- public:
- void setUp() override { d_context = new Context; }
-
- void tearDown() override { delete d_context; }
-
- 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();
-#ifdef CVC4_ASSERTIONS
- TS_UTILS_EXPECT_ABORT(d_context->pop());
- TS_UTILS_EXPECT_ABORT(d_context->pop());
-#endif /* CVC4_ASSERTIONS */
- }
-
- void testDtor() {
- // Destruction of ContextObj was broken in revision 324 (bug #45) when
- // at a higher context level with an intervening modification.
- // (The following caused a "pure virtual method called" error.)
- CDO<int> i(d_context);
- d_context->push();
- i = 5;
- }
-
- void testPrePostNotify() {
- // This is tricky; we want to detect if pre- and post-notifies are
- // done correctly. For that, we have to use a special ContextObj,
- // since that's the only thing that runs between pre- and post-.
-
- MyContextNotifyObj a(d_context, true), b(d_context, false);
-
- try {
- MyContextNotifyObj c(d_context, true), d(d_context, false);
-
- TS_ASSERT_EQUALS(a.nCalls, 0);
- TS_ASSERT_EQUALS(b.nCalls, 0);
- TS_ASSERT_EQUALS(c.nCalls, 0);
- TS_ASSERT_EQUALS(d.nCalls, 0);
-
- MyContextObj w(d_context, a);
- MyContextObj x(d_context, b);
- MyContextObj y(d_context, c);
- MyContextObj z(d_context, d);
-
- d_context->push();
-
- w.makeCurrent();
- x.makeCurrent();
- y.makeCurrent();
- z.makeCurrent();
-
- TS_ASSERT_EQUALS(a.nCalls, 0);
- TS_ASSERT_EQUALS(b.nCalls, 0);
- TS_ASSERT_EQUALS(c.nCalls, 0);
- TS_ASSERT_EQUALS(d.nCalls, 0);
-
- TS_ASSERT_EQUALS(w.nCalls, 0);
- TS_ASSERT_EQUALS(x.nCalls, 0);
- TS_ASSERT_EQUALS(y.nCalls, 0);
- TS_ASSERT_EQUALS(z.nCalls, 0);
-
- d_context->push();
-
- w.makeCurrent();
- x.makeCurrent();
- y.makeCurrent();
- z.makeCurrent();
-
- TS_ASSERT_EQUALS(a.nCalls, 0);
- TS_ASSERT_EQUALS(b.nCalls, 0);
- TS_ASSERT_EQUALS(c.nCalls, 0);
- TS_ASSERT_EQUALS(d.nCalls, 0);
-
- TS_ASSERT_EQUALS(w.nCalls, 0);
- TS_ASSERT_EQUALS(x.nCalls, 0);
- TS_ASSERT_EQUALS(y.nCalls, 0);
- TS_ASSERT_EQUALS(z.nCalls, 0);
-
- d_context->pop();
-
- TS_ASSERT_EQUALS(a.nCalls, 1);
- TS_ASSERT_EQUALS(b.nCalls, 1);
- TS_ASSERT_EQUALS(c.nCalls, 1);
- TS_ASSERT_EQUALS(d.nCalls, 1);
-
- TS_ASSERT_EQUALS(w.nCalls, 1);
- TS_ASSERT_EQUALS(x.nCalls, 0);
- TS_ASSERT_EQUALS(y.nCalls, 1);
- TS_ASSERT_EQUALS(z.nCalls, 0);
-
- d_context->pop();
-
- TS_ASSERT_EQUALS(a.nCalls, 2);
- TS_ASSERT_EQUALS(b.nCalls, 2);
- TS_ASSERT_EQUALS(c.nCalls, 2);
- TS_ASSERT_EQUALS(d.nCalls, 2);
-
- TS_ASSERT_EQUALS(w.nCalls, 2);
- TS_ASSERT_EQUALS(x.nCalls, 1);
- TS_ASSERT_EQUALS(y.nCalls, 2);
- TS_ASSERT_EQUALS(z.nCalls, 1);
- } catch(Exception& e) {
- cerr << e.toString() << endl;
- TS_FAIL("Exception thrown from test");
- }
-
- // we do this (together with the { } block above) to get full code
- // coverage of destruction paths; a and b haven't been destructed
- // yet, here.
- delete d_context;
-
- d_context = NULL;
- }
-
- void testTopScopeContextObj() {
- // this test's implementation is based on the fact that a
- // ContextObj allocated primordially "in the top scope" (first arg
- // to ctor is "true"), doesn't get updated if you immediately call
- // makeCurrent().
-
- MyContextNotifyObj n(d_context, true);
-
- d_context->push();
-
- MyContextObj x(true, d_context, n);
- MyContextObj y(false, d_context, n);
-
- TS_ASSERT_EQUALS(x.nSaves, 0);
- TS_ASSERT_EQUALS(y.nSaves, 0);
-
- x.makeCurrent();
- y.makeCurrent();
-
- TS_ASSERT_EQUALS(x.nSaves, 0);
- TS_ASSERT_EQUALS(y.nSaves, 1);
-
- d_context->push();
-
- x.makeCurrent();
- y.makeCurrent();
-
- TS_ASSERT_EQUALS(x.nSaves, 1);
- TS_ASSERT_EQUALS(y.nSaves, 2);
-
- d_context->pop();
- d_context->pop();
-
- TS_ASSERT_EQUALS(x.nSaves, 1);
- TS_ASSERT_EQUALS(y.nSaves, 2);
- }
-};