diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-12-04 12:07:51 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-12-04 12:07:51 -0800 |
commit | de6e4e0a2fc8e80574ccd2f271bd77c608791a00 (patch) | |
tree | 34c35369b8639bfbf797a429cffffabb45f04c96 | |
parent | 1636bd54a893ea9d1a559e0e6c45f184a8493209 (diff) |
google test: context: Migrate cdo_black. (#5586)
-rw-r--r-- | test/unit/context/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/unit/context/cdo_black.cpp | 51 | ||||
-rw-r--r-- | test/unit/context/cdo_black.h | 55 |
3 files changed, 52 insertions, 56 deletions
diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt index a9204033a..602ebc7df 100644 --- a/test/unit/context/CMakeLists.txt +++ b/test/unit/context/CMakeLists.txt @@ -14,7 +14,7 @@ cvc4_add_unit_test_black(cdlist_black context) cvc4_add_unit_test_black(cdmap_black context) cvc4_add_unit_test_white(cdmap_white context) -cvc4_add_cxx_unit_test_black(cdo_black context) +cvc4_add_unit_test_black(cdo_black context) cvc4_add_cxx_unit_test_black(context_black context) cvc4_add_cxx_unit_test_black(context_mm_black context) cvc4_add_cxx_unit_test_white(context_white context) diff --git a/test/unit/context/cdo_black.cpp b/test/unit/context/cdo_black.cpp new file mode 100644 index 000000000..440d95d40 --- /dev/null +++ b/test/unit/context/cdo_black.cpp @@ -0,0 +1,51 @@ +/********************* */ +/*! \file cdo_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, 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 Black box testing of CVC4::context::CDO<>. + ** + ** Black box testing of CVC4::context::CDO<>. + **/ + +#include <iostream> +#include <vector> + +#include "base/check.h" +#include "context/cdlist.h" +#include "context/cdo.h" +#include "test_context.h" + +namespace CVC4 { + +using namespace context; + +namespace test { + +class TestContextCDOBlack : public TestContext +{ +}; + +TEST_F(TestContextCDOBlack, cdo) +{ + // Test that push/pop maintains the original value + CDO<int> a1(d_context.get()); + a1 = 5; + EXPECT_EQ(d_context->getLevel(), 0); + d_context->push(); + a1 = 10; + EXPECT_EQ(d_context->getLevel(), 1); + EXPECT_EQ(a1, 10); + d_context->pop(); + EXPECT_EQ(d_context->getLevel(), 0); + EXPECT_EQ(a1, 5); +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h deleted file mode 100644 index 6c4540ae4..000000000 --- a/test/unit/context/cdo_black.h +++ /dev/null @@ -1,55 +0,0 @@ -/********************* */ -/*! \file cdo_black.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters, 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::CDO<>. - ** - ** Black box testing of CVC4::context::CDO<>. - **/ - -#include <cxxtest/TestSuite.h> - -#include <iostream> -#include <vector> - -#include "base/check.h" -#include "context/cdlist.h" -#include "context/cdo.h" -#include "context/context.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::context; - -class CDOBlack : public CxxTest::TestSuite { -private: - - Context* d_context; - - public: - void setUp() override { d_context = new Context; } - - void tearDown() override { delete d_context; } - - 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); - } -}; |