Naming scheme is `Test<directory><Black|White><name>`.
# Add unit tests
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_unit_test_black(cdhashmap_black context)
+cvc4_add_unit_test_white(cdhashmap_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)
--- /dev/null
+/********************* */
+/*! \file cdmap_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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::CDMap<>.
+ **
+ ** Black box testing of CVC4::context::CDMap<>.
+ **/
+
+#include <map>
+
+#include "base/check.h"
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
+#include "test_context.h"
+
+namespace CVC4 {
+namespace test {
+
+using CVC4::context::CDHashMap;
+using CVC4::context::Context;
+
+class TestContextBlackCDHashMap : public TestContext
+{
+ protected:
+ /** Returns the elements in a CDHashMap. */
+ static std::map<int32_t, int32_t> get_elements(
+ const CDHashMap<int32_t, int32_t>& map)
+ {
+ return std::map<int32_t, int32_t>{map.begin(), map.end()};
+ }
+
+ /**
+ * Returns true if the elements in map are the same as expected.
+ * NOTE: This is mostly to help the type checker for matching expected within
+ * a ASSERT_*.
+ */
+ static bool elements_are(const CDHashMap<int32_t, int32_t>& map,
+ const std::map<int32_t, int32_t>& expected)
+ {
+ return get_elements(map) == expected;
+ }
+};
+
+TEST_F(TestContextBlackCDHashMap, simple_sequence)
+{
+ CDHashMap<int32_t, int32_t> map(d_context.get());
+ ASSERT_TRUE(elements_are(map, {}));
+
+ map.insert(3, 4);
+ ASSERT_TRUE(elements_are(map, {{3, 4}}));
+
+ {
+ d_context->push();
+ ASSERT_TRUE(elements_are(map, {{3, 4}}));
+
+ map.insert(5, 6);
+ map.insert(9, 8);
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
+
+ {
+ d_context->push();
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
+
+ map.insert(1, 2);
+ ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
+
+ {
+ d_context->push();
+ ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
+
+ map.insertAtContextLevelZero(23, 317);
+ map.insert(1, 45);
+
+ ASSERT_TRUE(
+ elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+ map.insert(23, 324);
+
+ ASSERT_TRUE(
+ elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 324}}));
+ d_context->pop();
+ }
+
+ ASSERT_TRUE(
+ elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+ d_context->pop();
+ }
+
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+ d_context->pop();
+ }
+
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}}));
+}
+
+TEST_F(TestContextBlackCDHashMap, simple_sequence_fewer_finds)
+{
+ // no intervening find() in this one (under the theory that this could trigger
+ // a bug)
+ CDHashMap<int, int> map(d_context.get());
+ map.insert(3, 4);
+
+ {
+ d_context->push();
+
+ map.insert(5, 6);
+ map.insert(9, 8);
+
+ {
+ d_context->push();
+
+ map.insert(1, 2);
+
+ ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
+ {
+ d_context->push();
+ d_context->pop();
+ }
+
+ d_context->pop();
+ }
+
+ d_context->pop();
+ }
+}
+
+TEST_F(TestContextBlackCDHashMap, insert_at_context_level_zero)
+{
+ CDHashMap<int, int> map(d_context.get());
+
+ map.insert(3, 4);
+
+ ASSERT_TRUE(elements_are(map, {{3, 4}}));
+ {
+ d_context->push();
+ ASSERT_TRUE(elements_are(map, {{3, 4}}));
+
+ map.insert(5, 6);
+ map.insert(9, 8);
+
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
+
+ {
+ d_context->push();
+
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
+
+ map.insert(1, 2);
+
+ ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
+
+ map.insertAtContextLevelZero(23, 317);
+
+ ASSERT_TRUE(
+ elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+
+ ASSERT_DEATH(map.insertAtContextLevelZero(23, 317),
+ "insertAtContextLevelZero");
+ ASSERT_DEATH(map.insertAtContextLevelZero(23, 472),
+ "insertAtContextLevelZero");
+ map.insert(23, 472);
+
+ ASSERT_TRUE(
+ elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
+ {
+ d_context->push();
+
+ ASSERT_TRUE(
+ elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
+
+ ASSERT_DEATH(map.insertAtContextLevelZero(23, 0),
+ "insertAtContextLevelZero");
+ map.insert(23, 1024);
+
+ ASSERT_TRUE(
+ elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 1024}}));
+ d_context->pop();
+ }
+ ASSERT_TRUE(
+ elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
+ d_context->pop();
+ }
+
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
+
+ ASSERT_DEATH(map.insertAtContextLevelZero(23, 0),
+ "insertAtContextLevelZero");
+ map.insert(23, 477);
+
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}}));
+ d_context->pop();
+ }
+
+ ASSERT_DEATH(map.insertAtContextLevelZero(23, 0), "insertAtContextLevelZero");
+
+ ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}}));
+}
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file cdmap_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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::CDMap<>.
+ **
+ ** White box testing of CVC4::context::CDMap<>.
+ **/
+
+#include "base/check.h"
+#include "context/cdhashmap.h"
+#include "test_context.h"
+
+namespace CVC4 {
+
+using namespace context;
+
+namespace test {
+
+class TestContextWhiteCDHashMap : public TestContext
+{
+};
+
+TEST_F(TestContextWhiteCDHashMap, unreachable_save_and_restore)
+{
+ CDHashMap<int, int> map(d_context.get());
+
+ ASSERT_NO_THROW(map.makeCurrent());
+
+ ASSERT_DEATH(map.update(), "Unreachable code reached");
+
+ ASSERT_DEATH(map.save(d_context->getCMM()), "Unreachable code reached");
+ ASSERT_DEATH(map.restore(&map), "Unreachable code reached");
+
+ d_context->push();
+ ASSERT_DEATH(map.makeCurrent(), "Unreachable code reached");
+}
+
+} // namespace test
+} // namespace CVC4
~DtorSensitiveObject() { d_dtorCalled = true; }
};
-class TestContextCDListBlack : public TestContext
+class TestContextBlackCDList : public TestContext
{
protected:
void list_test(int n)
}
};
-TEST_F(TestContextCDListBlack, CDList10) { list_test(10); }
+TEST_F(TestContextBlackCDList, CDList10) { list_test(10); }
-TEST_F(TestContextCDListBlack, CDList15) { list_test(15); }
+TEST_F(TestContextBlackCDList, CDList15) { list_test(15); }
-TEST_F(TestContextCDListBlack, CDList20) { list_test(20); }
+TEST_F(TestContextBlackCDList, CDList20) { list_test(20); }
-TEST_F(TestContextCDListBlack, CDList35) { list_test(35); }
+TEST_F(TestContextBlackCDList, CDList35) { list_test(35); }
-TEST_F(TestContextCDListBlack, CDList50) { list_test(50); }
+TEST_F(TestContextBlackCDList, CDList50) { list_test(50); }
-TEST_F(TestContextCDListBlack, CDList99) { list_test(99); }
+TEST_F(TestContextBlackCDList, CDList99) { list_test(99); }
-TEST_F(TestContextCDListBlack, destructor_called)
+TEST_F(TestContextBlackCDList, destructor_called)
{
bool shouldRemainFalse = false;
bool shouldFlipToTrue = false;
ASSERT_EQ(aThirdFalse, false);
}
-TEST_F(TestContextCDListBlack, empty_iterator)
+TEST_F(TestContextBlackCDList, empty_iterator)
{
CDList<int>* list = new (true) CDList<int>(d_context.get());
ASSERT_EQ(list->begin(), list->end());
list->deleteSelf();
}
-TEST_F(TestContextCDListBlack, out_of_memory)
+TEST_F(TestContextBlackCDList, out_of_memory)
{
#ifndef CVC4_MEMORY_LIMITING_DISABLED
CDList<uint32_t> list(d_context.get());
#endif
}
-TEST_F(TestContextCDListBlack, pop_below_level_created)
+TEST_F(TestContextBlackCDList, pop_below_level_created)
{
d_context->push();
CDList<int32_t> list(d_context.get());
+++ /dev/null
-/********************* */
-/*! \file cdmap_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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::CDMap<>.
- **
- ** Black box testing of CVC4::context::CDMap<>.
- **/
-
-#include <map>
-
-#include "base/check.h"
-#include "context/cdhashmap.h"
-#include "context/cdlist.h"
-#include "test_context.h"
-
-namespace CVC4 {
-namespace test {
-
-using CVC4::context::CDHashMap;
-using CVC4::context::Context;
-
-class TestContextCDMapBlack : public TestContext
-{
- protected:
- /** Returns the elements in a CDHashMap. */
- static std::map<int32_t, int32_t> get_elements(
- const CDHashMap<int32_t, int32_t>& map)
- {
- return std::map<int32_t, int32_t>{map.begin(), map.end()};
- }
-
- /**
- * Returns true if the elements in map are the same as expected.
- * NOTE: This is mostly to help the type checker for matching expected within
- * a ASSERT_*.
- */
- static bool elements_are(const CDHashMap<int32_t, int32_t>& map,
- const std::map<int32_t, int32_t>& expected)
- {
- return get_elements(map) == expected;
- }
-};
-
-TEST_F(TestContextCDMapBlack, simple_sequence)
-{
- CDHashMap<int32_t, int32_t> map(d_context.get());
- ASSERT_TRUE(elements_are(map, {}));
-
- map.insert(3, 4);
- ASSERT_TRUE(elements_are(map, {{3, 4}}));
-
- {
- d_context->push();
- ASSERT_TRUE(elements_are(map, {{3, 4}}));
-
- map.insert(5, 6);
- map.insert(9, 8);
- ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
-
- {
- d_context->push();
- ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
-
- map.insert(1, 2);
- ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
-
- {
- d_context->push();
- ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
-
- map.insertAtContextLevelZero(23, 317);
- map.insert(1, 45);
-
- ASSERT_TRUE(
- elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
- map.insert(23, 324);
-
- ASSERT_TRUE(
- elements_are(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 324}}));
- d_context->pop();
- }
-
- ASSERT_TRUE(
- elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
- d_context->pop();
- }
-
- ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
- d_context->pop();
- }
-
- ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}}));
-}
-
-TEST_F(TestContextCDMapBlack, simple_sequence_fewer_finds)
-{
- // no intervening find() in this one (under the theory that this could trigger
- // a bug)
- CDHashMap<int, int> map(d_context.get());
- map.insert(3, 4);
-
- {
- d_context->push();
-
- map.insert(5, 6);
- map.insert(9, 8);
-
- {
- d_context->push();
-
- map.insert(1, 2);
-
- ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
- {
- d_context->push();
- d_context->pop();
- }
-
- d_context->pop();
- }
-
- d_context->pop();
- }
-}
-
-TEST_F(TestContextCDMapBlack, insert_at_context_level_zero)
-{
- CDHashMap<int, int> map(d_context.get());
-
- map.insert(3, 4);
-
- ASSERT_TRUE(elements_are(map, {{3, 4}}));
- {
- d_context->push();
- ASSERT_TRUE(elements_are(map, {{3, 4}}));
-
- map.insert(5, 6);
- map.insert(9, 8);
-
- ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
-
- {
- d_context->push();
-
- ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}}));
-
- map.insert(1, 2);
-
- ASSERT_TRUE(elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
-
- map.insertAtContextLevelZero(23, 317);
-
- ASSERT_TRUE(
- elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
-
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 317),
- "insertAtContextLevelZero");
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 472),
- "insertAtContextLevelZero");
- map.insert(23, 472);
-
- ASSERT_TRUE(
- elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
- {
- d_context->push();
-
- ASSERT_TRUE(
- elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
-
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 0),
- "insertAtContextLevelZero");
- map.insert(23, 1024);
-
- ASSERT_TRUE(
- elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 1024}}));
- d_context->pop();
- }
- ASSERT_TRUE(
- elements_are(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
- d_context->pop();
- }
-
- ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
-
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 0),
- "insertAtContextLevelZero");
- map.insert(23, 477);
-
- ASSERT_TRUE(elements_are(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}}));
- d_context->pop();
- }
-
- ASSERT_DEATH(map.insertAtContextLevelZero(23, 0), "insertAtContextLevelZero");
-
- ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}}));
-}
-} // namespace test
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file cdmap_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 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::CDMap<>.
- **
- ** White box testing of CVC4::context::CDMap<>.
- **/
-
-#include "base/check.h"
-#include "context/cdhashmap.h"
-#include "test_context.h"
-
-namespace CVC4 {
-
-using namespace context;
-
-namespace test {
-
-class TestContextCDMapWhite : public TestContext
-{
-};
-
-TEST_F(TestContextCDMapWhite, unreachable_save_and_restore)
-{
- CDHashMap<int, int> map(d_context.get());
-
- ASSERT_NO_THROW(map.makeCurrent());
-
- ASSERT_DEATH(map.update(), "Unreachable code reached");
-
- ASSERT_DEATH(map.save(d_context->getCMM()), "Unreachable code reached");
- ASSERT_DEATH(map.restore(&map), "Unreachable code reached");
-
- d_context->push();
- ASSERT_DEATH(map.makeCurrent(), "Unreachable code reached");
-}
-
-} // namespace test
-} // namespace CVC4
namespace test {
-class TestContextCDOBlack : public TestContext
+class TestContextBlackCDO : public TestContext
{
};
-TEST_F(TestContextCDOBlack, cdo)
+TEST_F(TestContextBlackCDO, cdo)
{
// Test that push/pop maintains the original value
CDO<int> a1(d_context.get());
namespace test {
-class TestContextMMBlack : public TestInternal
+class TestContextBlackMM : public TestInternal
{
protected:
void SetUp() override { d_cmm.reset(new ContextMemoryManager()); }
std::unique_ptr<ContextMemoryManager> d_cmm;
};
-TEST_F(TestContextMMBlack, push_pop)
+TEST_F(TestContextBlackMM, push_pop)
{
#ifdef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
#warning "Using the debug context memory manager, omitting unit tests"
projects / cvc5.git / commitdiff