From adc9bb5dff0c3d705b91d862d61a0c3057350688 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 9 Dec 2020 01:26:31 -0800 Subject: [PATCH] google test: context: Migrate context_white. (#5630) google test: context: Migrate context_white. --- test/unit/context/CMakeLists.txt | 2 +- test/unit/context/context_white.cpp | 183 +++++++++++++++++++++++++++ test/unit/context/context_white.h | 188 ---------------------------- 3 files changed, 184 insertions(+), 189 deletions(-) create mode 100644 test/unit/context/context_white.cpp delete mode 100644 test/unit/context/context_white.h diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt index 7d99fcbb2..6752f0e78 100644 --- a/test/unit/context/CMakeLists.txt +++ b/test/unit/context/CMakeLists.txt @@ -17,4 +17,4 @@ cvc4_add_unit_test_white(cdmap_white context) cvc4_add_unit_test_black(cdo_black context) cvc4_add_unit_test_black(context_black context) cvc4_add_unit_test_black(context_mm_black context) -cvc4_add_cxx_unit_test_white(context_white context) \ No newline at end of file +cvc4_add_unit_test_white(context_white context) diff --git a/test/unit/context/context_white.cpp b/test/unit/context/context_white.cpp new file mode 100644 index 000000000..c8ea59848 --- /dev/null +++ b/test/unit/context/context_white.cpp @@ -0,0 +1,183 @@ +/********************* */ +/*! \file context_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** 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 White box testing of CVC4::context::Context. + ** + ** White box testing of CVC4::context::Context. + **/ + +#include "base/check.h" +#include "context/cdo.h" +#include "test_context.h" + +namespace CVC4 { + +using namespace context; + +namespace test { + +class TestContextWhite : public TestContext +{ +}; + +TEST_F(TestContextWhite, simple) +{ + Scope* s = d_context->getTopScope(); + + EXPECT_EQ(s, d_context->getBottomScope()); + EXPECT_EQ(d_context->getLevel(), 0); + EXPECT_EQ(d_context->d_scopeList.size(), 1); + + EXPECT_EQ(s->d_pContext, d_context.get()); + EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); + EXPECT_EQ(s->d_level, 0); + EXPECT_EQ(s->d_pContextObjList, nullptr); + + CDO a(d_context.get()); + + EXPECT_EQ(s->d_pContext, d_context.get()); + EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); + EXPECT_EQ(s->d_level, 0); + EXPECT_EQ(s->d_pContextObjList, &a); + + EXPECT_EQ(a.d_pScope, s); + EXPECT_EQ(a.d_pContextObjRestore, nullptr); + EXPECT_EQ(a.d_pContextObjNext, nullptr); + EXPECT_EQ(a.d_ppContextObjPrev, &s->d_pContextObjList); + + CDO b(d_context.get()); + + EXPECT_EQ(s->d_pContext, d_context.get()); + EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); + EXPECT_EQ(s->d_level, 0); + EXPECT_EQ(s->d_pContextObjList, &b); + + EXPECT_EQ(a.d_pScope, s); + EXPECT_EQ(a.d_pContextObjRestore, nullptr); + EXPECT_EQ(a.d_pContextObjNext, nullptr); + EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + + EXPECT_EQ(b.d_pScope, s); + EXPECT_EQ(b.d_pContextObjRestore, nullptr); + EXPECT_EQ(b.d_pContextObjNext, &a); + EXPECT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList); + + d_context->push(); + Scope* t = d_context->getTopScope(); + EXPECT_NE(s, t); + + EXPECT_EQ(s, d_context->getBottomScope()); + EXPECT_EQ(d_context->getLevel(), 1); + EXPECT_EQ(d_context->d_scopeList.size(), 2); + + EXPECT_EQ(s->d_pContext, d_context.get()); + EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); + EXPECT_EQ(s->d_level, 0); + EXPECT_EQ(s->d_pContextObjList, &b); + + EXPECT_EQ(t->d_pContext, d_context.get()); + EXPECT_EQ(t->d_pCMM, d_context->d_pCMM); + EXPECT_EQ(t->d_level, 1); + EXPECT_EQ(t->d_pContextObjList, nullptr); + + EXPECT_EQ(a.d_pScope, s); + EXPECT_EQ(a.d_pContextObjRestore, nullptr); + EXPECT_EQ(a.d_pContextObjNext, nullptr); + EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + + EXPECT_EQ(b.d_pScope, s); + EXPECT_EQ(b.d_pContextObjRestore, nullptr); + EXPECT_EQ(b.d_pContextObjNext, &a); + EXPECT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList); + + a = 5; + + EXPECT_EQ(t->d_pContext, d_context.get()); + EXPECT_EQ(t->d_pCMM, d_context->d_pCMM); + EXPECT_EQ(t->d_level, 1); + EXPECT_EQ(t->d_pContextObjList, &a); + + EXPECT_EQ(a.d_pScope, t); + EXPECT_NE(a.d_pContextObjRestore, nullptr); + EXPECT_EQ(a.d_pContextObjNext, nullptr); + EXPECT_EQ(a.d_ppContextObjPrev, &t->d_pContextObjList); + + b = 3; + + EXPECT_EQ(t->d_pContext, d_context.get()); + EXPECT_EQ(t->d_pCMM, d_context->d_pCMM); + EXPECT_EQ(t->d_level, 1); + EXPECT_EQ(t->d_pContextObjList, &b); + + EXPECT_EQ(a.d_pScope, t); + EXPECT_NE(a.d_pContextObjRestore, nullptr); + EXPECT_EQ(a.d_pContextObjNext, nullptr); + EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + + EXPECT_EQ(b.d_pScope, t); + EXPECT_NE(b.d_pContextObjRestore, nullptr); + EXPECT_EQ(b.d_pContextObjNext, &a); + EXPECT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList); + + d_context->push(); + Scope* u = d_context->getTopScope(); + EXPECT_NE(u, t); + EXPECT_NE(u, s); + + CDO c(d_context.get()); + c = 4; + + EXPECT_EQ(c.d_pScope, u); + EXPECT_NE(c.d_pContextObjRestore, nullptr); + EXPECT_EQ(c.d_pContextObjNext, nullptr); + EXPECT_EQ(c.d_ppContextObjPrev, &u->d_pContextObjList); + + d_context->pop(); + + EXPECT_EQ(t->d_pContext, d_context.get()); + EXPECT_EQ(t->d_pCMM, d_context->d_pCMM); + EXPECT_EQ(t->d_level, 1); + EXPECT_EQ(t->d_pContextObjList, &b); + + EXPECT_EQ(a.d_pScope, t); + EXPECT_NE(a.d_pContextObjRestore, nullptr); + EXPECT_EQ(a.d_pContextObjNext, nullptr); + EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + + EXPECT_EQ(b.d_pScope, t); + EXPECT_NE(b.d_pContextObjRestore, nullptr); + EXPECT_EQ(b.d_pContextObjNext, &a); + EXPECT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList); + + d_context->pop(); + + EXPECT_EQ(s->d_pContext, d_context.get()); + EXPECT_EQ(s->d_pCMM, d_context->d_pCMM); + EXPECT_EQ(s->d_level, 0); + EXPECT_EQ(s->d_pContextObjList, &c); + + EXPECT_EQ(a.d_pScope, s); + EXPECT_EQ(a.d_pContextObjRestore, nullptr); + EXPECT_EQ(a.d_pContextObjNext, nullptr); + EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext); + + EXPECT_EQ(b.d_pScope, s); + EXPECT_EQ(b.d_pContextObjRestore, nullptr); + EXPECT_EQ(b.d_pContextObjNext, &a); + EXPECT_EQ(b.d_ppContextObjPrev, &c.d_pContextObjNext); + + EXPECT_EQ(c.d_pScope, s); + EXPECT_EQ(c.d_pContextObjRestore, nullptr); + EXPECT_EQ(c.d_pContextObjNext, &b); + EXPECT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h deleted file mode 100644 index 4fd0f8d7f..000000000 --- a/test/unit/context/context_white.h +++ /dev/null @@ -1,188 +0,0 @@ -/********************* */ -/*! \file context_white.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Dejan Jovanovic - ** 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 White box testing of CVC4::context::Context. - ** - ** White box testing of CVC4::context::Context. - **/ - -#include - -#include "base/check.h" -#include "context/cdo.h" -#include "context/context.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::context; - -class ContextWhite : public CxxTest::TestSuite { -private: - - Context* d_context; - - public: - void setUp() override { d_context = new Context; } - - void tearDown() override { delete d_context; } - - void testContextSimple() - { - Scope* s = d_context->getTopScope(); - - TS_ASSERT(s == d_context->getBottomScope()); - TS_ASSERT(d_context->getLevel() == 0); - TS_ASSERT(d_context->d_scopeList.size() == 1); - - TS_ASSERT(s->d_pContext == d_context); - TS_ASSERT(s->d_pCMM == d_context->d_pCMM); - TS_ASSERT(s->d_level == 0); - TS_ASSERT(s->d_pContextObjList == NULL); - - CDO a(d_context); - - TS_ASSERT(s->d_pContext == d_context); - TS_ASSERT(s->d_pCMM == d_context->d_pCMM); - TS_ASSERT(s->d_level == 0); - TS_ASSERT(s->d_pContextObjList == &a); - - TS_ASSERT(a.d_pScope == s); - TS_ASSERT(a.d_pContextObjRestore == NULL); - TS_ASSERT(a.d_pContextObjNext == NULL); - TS_ASSERT(a.d_ppContextObjPrev == &s->d_pContextObjList); - - CDO b(d_context); - - TS_ASSERT(s->d_pContext == d_context); - TS_ASSERT(s->d_pCMM == d_context->d_pCMM); - TS_ASSERT(s->d_level == 0); - TS_ASSERT(s->d_pContextObjList == &b); - - TS_ASSERT(a.d_pScope == s); - TS_ASSERT(a.d_pContextObjRestore == NULL); - TS_ASSERT(a.d_pContextObjNext == NULL); - TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); - - TS_ASSERT(b.d_pScope == s); - TS_ASSERT(b.d_pContextObjRestore == NULL); - TS_ASSERT(b.d_pContextObjNext == &a); - TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); - - d_context->push(); - Scope* t = d_context->getTopScope(); - TS_ASSERT(s != t); - - TS_ASSERT(s == d_context->getBottomScope()); - TS_ASSERT(d_context->getLevel() == 1); - TS_ASSERT(d_context->d_scopeList.size() == 2); - - TS_ASSERT(s->d_pContext == d_context); - TS_ASSERT(s->d_pCMM == d_context->d_pCMM); - TS_ASSERT(s->d_level == 0); - TS_ASSERT(s->d_pContextObjList == &b); - - TS_ASSERT(t->d_pContext == d_context); - TS_ASSERT(t->d_pCMM == d_context->d_pCMM); - TS_ASSERT(t->d_level == 1); - TS_ASSERT(t->d_pContextObjList == NULL); - - TS_ASSERT(a.d_pScope == s); - TS_ASSERT(a.d_pContextObjRestore == NULL); - TS_ASSERT(a.d_pContextObjNext == NULL); - TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); - - TS_ASSERT(b.d_pScope == s); - TS_ASSERT(b.d_pContextObjRestore == NULL); - TS_ASSERT(b.d_pContextObjNext == &a); - TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); - - a = 5; - - TS_ASSERT(t->d_pContext == d_context); - TS_ASSERT(t->d_pCMM == d_context->d_pCMM); - TS_ASSERT(t->d_level == 1); - TS_ASSERT(t->d_pContextObjList == &a); - - TS_ASSERT(a.d_pScope == t); - TS_ASSERT(a.d_pContextObjRestore != NULL); - TS_ASSERT(a.d_pContextObjNext == NULL); - TS_ASSERT(a.d_ppContextObjPrev == &t->d_pContextObjList); - - b = 3; - - TS_ASSERT(t->d_pContext == d_context); - TS_ASSERT(t->d_pCMM == d_context->d_pCMM); - TS_ASSERT(t->d_level == 1); - TS_ASSERT(t->d_pContextObjList == &b); - - TS_ASSERT(a.d_pScope == t); - TS_ASSERT(a.d_pContextObjRestore != NULL); - TS_ASSERT(a.d_pContextObjNext == NULL); - TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); - - TS_ASSERT(b.d_pScope == t); - TS_ASSERT(b.d_pContextObjRestore != NULL); - TS_ASSERT(b.d_pContextObjNext == &a); - TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList); - - d_context->push(); - Scope* u = d_context->getTopScope(); - TS_ASSERT(u != t); - TS_ASSERT(u != s); - - CDO c(d_context); - c = 4; - - TS_ASSERT(c.d_pScope == u); - TS_ASSERT(c.d_pContextObjRestore != NULL); - TS_ASSERT(c.d_pContextObjNext == NULL); - TS_ASSERT(c.d_ppContextObjPrev == &u->d_pContextObjList); - - d_context->pop(); - - TS_ASSERT(t->d_pContext == d_context); - TS_ASSERT(t->d_pCMM == d_context->d_pCMM); - TS_ASSERT(t->d_level == 1); - TS_ASSERT(t->d_pContextObjList == &b); - - TS_ASSERT(a.d_pScope == t); - TS_ASSERT(a.d_pContextObjRestore != NULL); - TS_ASSERT(a.d_pContextObjNext == NULL); - TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); - - TS_ASSERT(b.d_pScope == t); - TS_ASSERT(b.d_pContextObjRestore != NULL); - TS_ASSERT(b.d_pContextObjNext == &a); - TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList); - - d_context->pop(); - - TS_ASSERT(s->d_pContext == d_context); - TS_ASSERT(s->d_pCMM == d_context->d_pCMM); - TS_ASSERT(s->d_level == 0); - TS_ASSERT(s->d_pContextObjList == &c); - - TS_ASSERT(a.d_pScope == s); - TS_ASSERT(a.d_pContextObjRestore == NULL); - TS_ASSERT(a.d_pContextObjNext == NULL); - TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); - - TS_ASSERT(b.d_pScope == s); - TS_ASSERT(b.d_pContextObjRestore == NULL); - TS_ASSERT(b.d_pContextObjNext == &a); - TS_ASSERT(b.d_ppContextObjPrev == &c.d_pContextObjNext); - - TS_ASSERT(c.d_pScope == s); - TS_ASSERT(c.d_pContextObjRestore == NULL); - TS_ASSERT(c.d_pContextObjNext == &b); - TS_ASSERT(c.d_ppContextObjPrev == &s->d_pContextObjList); - } -}; -- 2.30.2