diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /test/unit | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'test/unit')
24 files changed, 162 insertions, 217 deletions
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 6c5ecdf08..96c575218 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -18,12 +18,12 @@ #include <map> -#include "base/cvc4_assert.h" -#include "context/context.h" +#include "base/check.h" #include "context/cdhashmap.h" #include "context/cdlist.h" +#include "context/context.h" +#include "test_utils.h" -using CVC4::AssertionException; using CVC4::context::Context; using CVC4::context::CDHashMap; @@ -163,10 +163,8 @@ class CDMapBlack : public CxxTest::TestSuite { TS_ASSERT( ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}})); - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317), - AssertionException&); - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472), - AssertionException&); + TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 317)); + TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 472)); map.insert(23, 472); TS_ASSERT( @@ -177,8 +175,7 @@ class CDMapBlack : public CxxTest::TestSuite { TS_ASSERT( ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}})); - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), - AssertionException&); + TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 0)); map.insert(23, 1024); TS_ASSERT( @@ -194,8 +191,7 @@ class CDMapBlack : public CxxTest::TestSuite { TS_ASSERT( ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}})); - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), - AssertionException&); + TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 0)); map.insert(23, 477); TS_ASSERT( @@ -203,7 +199,7 @@ class CDMapBlack : public CxxTest::TestSuite { d_context->pop(); } - TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException&); + TS_UTILS_EXPECT_ABORT(map.insertAtContextLevelZero(23, 0)); TS_ASSERT( ElementsAre(map, {{3, 4}, {23, 317}})); diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index 1a1f683bc..d22ecc7f1 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -16,8 +16,9 @@ #include <cxxtest/TestSuite.h> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "context/cdhashmap.h" +#include "test_utils.h" using namespace std; using namespace CVC4; @@ -38,12 +39,12 @@ class CDMapWhite : public CxxTest::TestSuite { TS_ASSERT_THROWS_NOTHING(map.makeCurrent()); - TS_ASSERT_THROWS(map.update(), UnreachableCodeException&); + TS_UTILS_EXPECT_ABORT(map.update()); - TS_ASSERT_THROWS(map.save(d_context->getCMM()), UnreachableCodeException&); - TS_ASSERT_THROWS(map.restore(&map), UnreachableCodeException&); + TS_UTILS_EXPECT_ABORT(map.save(d_context->getCMM())); + TS_UTILS_EXPECT_ABORT(map.restore(&map)); d_context->push(); - TS_ASSERT_THROWS(map.makeCurrent(), UnreachableCodeException&); + TS_UTILS_EXPECT_ABORT(map.makeCurrent()); } }; diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h index 4f927abfc..4e1efb7b1 100644 --- a/test/unit/context/cdo_black.h +++ b/test/unit/context/cdo_black.h @@ -19,7 +19,7 @@ #include <iostream> #include <vector> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "context/cdlist.h" #include "context/cdo.h" #include "context/context.h" diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index 3659d3494..258c3fd9b 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -19,11 +19,11 @@ #include <iostream> #include <vector> -#include "base/cvc4_assert.h" +#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; @@ -106,8 +106,8 @@ private: d_context->push(); d_context->pop(); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(d_context->pop(), AssertionException&); - TS_ASSERT_THROWS(d_context->pop(), AssertionException&); + TS_UTILS_EXPECT_ABORT(d_context->pop()); + TS_UTILS_EXPECT_ABORT(d_context->pop()); #endif /* CVC4_ASSERTIONS */ } diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index 15f9b09de..cd5ff8242 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -22,8 +22,7 @@ #include <iostream> #include "context/context_mm.h" - -#include "base/cvc4_assert.h" +#include "test_utils.h" using namespace std; using namespace CVC4::context; @@ -90,7 +89,7 @@ private: } // Try popping out of scope - TS_ASSERT_THROWS(d_cmm->pop(), CVC4::AssertionException&); + TS_UTILS_EXPECT_ABORT(d_cmm->pop()); #endif /* __CVC4__CONTEXT__CONTEXT_MM_H */ } diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h index 515ffb848..87ff73cce 100644 --- a/test/unit/context/context_white.h +++ b/test/unit/context/context_white.h @@ -16,9 +16,9 @@ #include <cxxtest/TestSuite.h> -#include "base/cvc4_assert.h" -#include "context/context.h" +#include "base/check.h" #include "context/cdo.h" +#include "context/context.h" using namespace std; using namespace CVC4; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index d109efdfd..745264b83 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -18,7 +18,7 @@ #include <string> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/attribute.h" #include "expr/node.h" #include "expr/node_builder.h" diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 287704f39..e4a0dbb36 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -27,6 +27,7 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node_value.h" +#include "test_utils.h" using namespace CVC4; using namespace CVC4::kind; @@ -179,8 +180,8 @@ class NodeBlack : public CxxTest::TestSuite { #ifdef CVC4_ASSERTIONS // Basic bounds check on a node w/out children - TS_ASSERT_THROWS(Node::null()[-1], AssertionException&); - TS_ASSERT_THROWS(Node::null()[0], AssertionException&); + TS_UTILS_EXPECT_ABORT(Node::null()[-1]); + TS_UTILS_EXPECT_ABORT(Node::null()[0]); #endif /* CVC4_ASSERTIONS */ // Basic access check @@ -198,8 +199,8 @@ class NodeBlack : public CxxTest::TestSuite { #ifdef CVC4_ASSERTIONS // Bounds check on a node with children - TS_ASSERT_THROWS(ite == ite[-1], AssertionException&); - TS_ASSERT_THROWS(ite == ite[4], AssertionException&); + TS_UTILS_EXPECT_ABORT(ite == ite[-1]); + TS_UTILS_EXPECT_ABORT(ite == ite[4]); #endif /* CVC4_ASSERTIONS */ } @@ -459,10 +460,10 @@ class NodeBlack : public CxxTest::TestSuite { } #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(testNaryExpForSize(AND, 0), AssertionException&); - TS_ASSERT_THROWS(testNaryExpForSize(AND, 1), AssertionException&); - TS_ASSERT_THROWS(testNaryExpForSize(NOT, 0), AssertionException&); - TS_ASSERT_THROWS(testNaryExpForSize(NOT, 2), AssertionException&); + TS_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 0)); + TS_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 1)); + TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 0)); + TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 2)); #endif /* CVC4_ASSERTIONS */ } diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 2ece96cb8..473557e07 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -20,11 +20,12 @@ #include <limits.h> #include <sstream> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/kind.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" +#include "test_utils.h" #include "util/rational.h" using namespace CVC4; @@ -90,9 +91,9 @@ private: NodeBuilder<> def; TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(def.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(def.begin(), AssertionException&); - TS_ASSERT_THROWS(def.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(def.getNumChildren()); + TS_UTILS_EXPECT_ABORT(def.begin()); + TS_UTILS_EXPECT_ABORT(def.end()); #endif /* CVC4_ASSERTIONS */ NodeBuilder<> spec(specKind); @@ -104,9 +105,9 @@ private: NodeBuilder<> from_nm(d_nm); TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(from_nm.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(from_nm.begin(), AssertionException&); - TS_ASSERT_THROWS(from_nm.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(from_nm.getNumChildren()); + TS_UTILS_EXPECT_ABORT(from_nm.begin()); + TS_UTILS_EXPECT_ABORT(from_nm.end()); #endif /* CVC4_ASSERTIONS */ NodeBuilder<> from_nm_kind(d_nm, specKind); @@ -120,9 +121,9 @@ private: NodeBuilder<K> ws; TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(ws.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(ws.begin(), AssertionException&); - TS_ASSERT_THROWS(ws.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(ws.getNumChildren()); + TS_UTILS_EXPECT_ABORT(ws.begin()); + TS_UTILS_EXPECT_ABORT(ws.end()); #endif /* CVC4_ASSERTIONS */ NodeBuilder<K> ws_kind(specKind); @@ -134,9 +135,9 @@ private: NodeBuilder<K> ws_from_nm(d_nm); TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(ws_from_nm.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(ws_from_nm.begin(), AssertionException&); - TS_ASSERT_THROWS(ws_from_nm.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(ws_from_nm.getNumChildren()); + TS_UTILS_EXPECT_ABORT(ws_from_nm.begin()); + TS_UTILS_EXPECT_ABORT(ws_from_nm.end()); #endif /* CVC4_ASSERTIONS */ NodeBuilder<K> ws_from_nm_kind(d_nm, specKind); @@ -158,33 +159,33 @@ private: NodeBuilder<> copy(def); TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(copy.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(copy.begin(), AssertionException&); - TS_ASSERT_THROWS(copy.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(copy.getNumChildren()); + TS_UTILS_EXPECT_ABORT(copy.begin()); + TS_UTILS_EXPECT_ABORT(copy.end()); #endif /* CVC4_ASSERTIONS */ NodeBuilder<K> cp_ws(ws); TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(cp_ws.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(cp_ws.begin(), AssertionException&); - TS_ASSERT_THROWS(cp_ws.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(cp_ws.getNumChildren()); + TS_UTILS_EXPECT_ABORT(cp_ws.begin()); + TS_UTILS_EXPECT_ABORT(cp_ws.end()); #endif /* CVC4_ASSERTIONS */ NodeBuilder<K-10> cp_from_larger(ws); TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(cp_from_larger.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(cp_from_larger.begin(), AssertionException&); - TS_ASSERT_THROWS(cp_from_larger.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(cp_from_larger.getNumChildren()); + TS_UTILS_EXPECT_ABORT(cp_from_larger.begin()); + TS_UTILS_EXPECT_ABORT(cp_from_larger.end()); #endif /* CVC4_ASSERTIONS */ NodeBuilder<K+10> cp_from_smaller(ws); TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(cp_from_smaller.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(cp_from_smaller.begin(), AssertionException&); - TS_ASSERT_THROWS(cp_from_smaller.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(cp_from_smaller.getNumChildren()); + TS_UTILS_EXPECT_ABORT(cp_from_smaller.begin()); + TS_UTILS_EXPECT_ABORT(cp_from_smaller.end()); #endif /* CVC4_ASSERTIONS */ } @@ -282,7 +283,7 @@ private: Node n = noKind; #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(noKind.getKind(), AssertionException&); + TS_UTILS_EXPECT_ABORT(noKind.getKind()); #endif /* CVC4_ASSERTIONS */ NodeBuilder<> spec(PLUS); @@ -297,7 +298,7 @@ private: NodeBuilder<> nb; #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&); + TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); #endif /* CVC4_ASSERTIONS */ nb << PLUS << x << x; @@ -309,7 +310,7 @@ private: Node n = nb;// avoid warning on clear() nb.clear(); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&); + TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); #endif /* CVC4_ASSERTIONS */ nb.clear(PLUS); TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); @@ -321,16 +322,16 @@ private: TS_ASSERT_EQUALS(nb.getNumChildren(), 6u); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb << PLUS, AssertionException&); + TS_UTILS_EXPECT_ABORT(nb << PLUS); n = nb; - TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&); + TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); #endif /* CVC4_ASSERTIONS */ } void testOperatorSquare() { /* Node operator[](int i) const { - Assert(i >= 0 && i < d_ev->getNumChildren()); + TS_ASSERT(i >= 0 && i < d_ev->getNumChildren()); return Node(d_ev->d_children[i]); } */ @@ -341,8 +342,8 @@ private: Node i_K = d_nm->mkNode(NOT, i_0); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(arr[-1], AssertionException&); - TS_ASSERT_THROWS(arr[0], AssertionException&); + TS_UTILS_EXPECT_ABORT(arr[-1]); + TS_UTILS_EXPECT_ABORT(arr[0]); #endif /* CVC4_ASSERTIONS */ arr << i_0; @@ -375,7 +376,7 @@ private: #ifdef CVC4_ASSERTIONS Node n = arr; - TS_ASSERT_THROWS(arr[0], AssertionException&); + TS_UTILS_EXPECT_ABORT(arr[0]); #endif /* CVC4_ASSERTIONS */ } @@ -385,9 +386,9 @@ private: TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(nb.begin(), AssertionException&); - TS_ASSERT_THROWS(nb.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); + TS_UTILS_EXPECT_ABORT(nb.begin()); + TS_UTILS_EXPECT_ABORT(nb.end()); #endif /* CVC4_ASSERTIONS */ nb << specKind; @@ -402,9 +403,9 @@ private: TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(nb.begin(), AssertionException&); - TS_ASSERT_THROWS(nb.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); + TS_UTILS_EXPECT_ABORT(nb.begin()); + TS_UTILS_EXPECT_ABORT(nb.end()); #endif /* CVC4_ASSERTIONS */ nb << specKind; @@ -427,9 +428,9 @@ private: TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb.getNumChildren(), AssertionException&); - TS_ASSERT_THROWS(nb.begin(), AssertionException&); - TS_ASSERT_THROWS(nb.end(), AssertionException&); + TS_UTILS_EXPECT_ABORT(nb.getNumChildren()); + TS_UTILS_EXPECT_ABORT(nb.begin()); + TS_UTILS_EXPECT_ABORT(nb.end()); #endif /* CVC4_ASSERTIONS */ } @@ -438,7 +439,7 @@ private: #ifdef CVC4_ASSERTIONS NodeBuilder<> spec(specKind); - TS_ASSERT_THROWS(spec << PLUS, AssertionException&); + TS_UTILS_EXPECT_ABORT(spec << PLUS); #endif /* CVC4_ASSERTIONS */ NodeBuilder<> noSpec; @@ -457,12 +458,12 @@ private: nb.clear(PLUS); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(n = nb, AssertionException&); + TS_UTILS_EXPECT_ABORT(n = nb); nb.clear(PLUS); #endif /* CVC4_ASSERTIONS */ #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb << PLUS, AssertionException&); + TS_UTILS_EXPECT_ABORT(nb << PLUS); #endif /* CVC4_ASSERTIONS */ NodeBuilder<> testRef; @@ -470,7 +471,7 @@ private: #ifdef CVC4_ASSERTIONS NodeBuilder<> testTwo; - TS_ASSERT_THROWS(testTwo << specKind << PLUS, AssertionException&); + TS_UTILS_EXPECT_ABORT(testTwo << specKind << PLUS); #endif /* CVC4_ASSERTIONS */ NodeBuilder<> testMixOrder1; @@ -494,7 +495,7 @@ private: #ifdef CVC4_ASSERTIONS Node n = nb; - TS_ASSERT_THROWS(nb << n, AssertionException&); + TS_UTILS_EXPECT_ABORT(nb << n); #endif /* CVC4_ASSERTIONS */ NodeBuilder<> overflow(specKind); @@ -527,7 +528,7 @@ private: Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y)); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(d_nm->mkNode(XOR, y, x, x), AssertionException&); + TS_UTILS_EXPECT_ABORT(d_nm->mkNode(XOR, y, x, x)); #endif /* CVC4_ASSERTIONS */ NodeBuilder<> b(specKind); @@ -588,7 +589,7 @@ private: TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(Node blah = implicit, AssertionException&); + TS_UTILS_EXPECT_ABORT(Node blah = implicit); #endif /* CVC4_ASSERTIONS */ } diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index e568fc9df..4b9c42bd0 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -22,6 +22,7 @@ #include "base/output.h" #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" +#include "test_utils.h" #include "util/integer.h" #include "util/rational.h" @@ -300,7 +301,7 @@ class NodeManagerBlack : public CxxTest::TestSuite { void testMkNodeTooFew() { #ifdef CVC4_ASSERTIONS Node x = d_nodeManager->mkSkolem( "x", d_nodeManager->booleanType() ); - TS_ASSERT_THROWS(d_nodeManager->mkNode(AND, x), AssertionException&); + TS_UTILS_EXPECT_ABORT(d_nodeManager->mkNode(AND, x)); #endif } @@ -319,7 +320,7 @@ class NodeManagerBlack : public CxxTest::TestSuite { vars.push_back(skolem_j); vars.push_back(orNode); } - TS_ASSERT_THROWS(d_nodeManager->mkNode(AND, vars), AssertionException&); + TS_UTILS_EXPECT_ABORT(d_nodeManager->mkNode(AND, vars)); #endif } }; diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index c2888a708..6f7729f74 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -19,6 +19,7 @@ #include <string> #include "expr/node_manager.h" +#include "test_utils.h" #include "util/integer.h" #include "util/rational.h" @@ -57,7 +58,7 @@ class NodeManagerWhite : public CxxTest::TestSuite { TS_ASSERT_THROWS_NOTHING(nb.realloc(25)); TS_ASSERT_THROWS_NOTHING(nb.realloc(256)); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb.realloc(100), AssertionException&); + TS_UTILS_EXPECT_ABORT(nb.realloc(100)); #endif /* CVC4_ASSERTIONS */ TS_ASSERT_THROWS_NOTHING(nb.realloc(257)); TS_ASSERT_THROWS_NOTHING(nb.realloc(4000)); @@ -67,7 +68,7 @@ class NodeManagerWhite : public CxxTest::TestSuite { TS_ASSERT_THROWS_NOTHING(nb.realloc(65536)); TS_ASSERT_THROWS_NOTHING(nb.realloc(67108863)); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(nb.realloc(67108863), AssertionException&); + TS_UTILS_EXPECT_ABORT(nb.realloc(67108863)); #endif /* CVC4_ASSERTIONS */ } diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index e9a3112cf..c95c46e02 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -18,7 +18,7 @@ #include <string> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index ef65e8773..1ac1fa315 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -19,7 +19,7 @@ #include <sstream> #include <string> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/exception.h" #include "context/context.h" #include "expr/expr.h" diff --git a/test/unit/memory.h b/test/unit/memory.h index 49b0885b1..9c92ba918 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -36,8 +36,8 @@ #include <sys/resource.h> #include <sys/time.h> +#include "base/check.h" #include "base/configuration_private.h" -#include "base/cvc4_assert.h" // Conditionally define CVC4_MEMORY_LIMITING_DISABLED. #ifdef __APPLE__ diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h index 7f7af40b9..4037c7191 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -20,6 +20,7 @@ #include "preprocessing/passes/bv_gauss.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" +#include "test_utils.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "util/bitvector.h" @@ -116,14 +117,6 @@ static void testGaussElimX(Integer prime, } } -template <class T> -static void testGaussElimT(Integer prime, - std::vector<Integer> rhs, - std::vector<std::vector<Integer>> lhs) -{ - TS_ASSERT_THROWS(BVGauss::gaussElim(prime, rhs, lhs), T); -} - class TheoryBVGaussWhite : public CxxTest::TestSuite { ExprManager *d_em; @@ -319,7 +312,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite {Integer(2), Integer(3), Integer(5)}, {Integer(4), Integer(0), Integer(5)}}; std::cout << "matrix 0, modulo 0" << std::endl; // throws - testGaussElimT<AssertionException>(Integer(0), rhs, lhs); + TS_UTILS_EXPECT_ABORT(BVGauss::gaussElim(Integer(0), rhs, lhs)); std::cout << "matrix 0, modulo 1" << std::endl; testGaussElimX(Integer(1), rhs, lhs, BVGauss::Result::UNIQUE); std::cout << "matrix 0, modulo 2" << std::endl; diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index 7aaf1f4de..70357ea1b 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -18,7 +18,7 @@ /* #include <gmock/gmock.h> */ /* #include <gtest/gtest.h> */ -#include "base/cvc4_assert.h" +#include "base/check.h" #include "context/context.h" #include "expr/expr_manager.h" #include "expr/node_manager.h" diff --git a/test/unit/test_utils.h b/test/unit/test_utils.h index 67bc34456..474f2e78b 100644 --- a/test/unit/test_utils.h +++ b/test/unit/test_utils.h @@ -18,7 +18,7 @@ /** * Use TS_UTILS_EXPECT_ABORT if you expect the expression to abort() when a - * CVC4_CHECK or CVC4_DCHECK is triggered. + * AlwaysAssert or Assert is triggered. */ #define TS_UTILS_EXPECT_ABORT(expr) \ do \ diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index d357b200e..88f8ed6dd 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -25,7 +25,7 @@ #include <memory> #include <string> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "context/context.h" #include "expr/kind.h" #include "expr/node.h" diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index 5be92b19e..03fcaab69 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -47,9 +47,9 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite Node x, Node (*getsc)(bool, Kind, Node, Node)) { - Assert(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL - || k == BITVECTOR_UGT || k == BITVECTOR_SGT); - Assert(k != EQUAL || pol == false); + TS_ASSERT(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL + || k == BITVECTOR_UGT || k == BITVECTOR_SGT); + TS_ASSERT(k != EQUAL || pol == false); Node sc = getsc(pol, k, d_sk, d_t); Kind ksc = sc.getKind(); @@ -78,7 +78,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite } else { - Assert(k == EQUAL); + TS_ASSERT(k == EQUAL); k = DISTINCT; } } @@ -95,10 +95,10 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite unsigned idx, Node (*getsc)(bool, Kind, Kind, unsigned, Node, Node, Node)) { - Assert(k == BITVECTOR_MULT || k == BITVECTOR_UREM_TOTAL - || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND - || k == BITVECTOR_OR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR - || k == BITVECTOR_SHL); + TS_ASSERT(k == BITVECTOR_MULT || k == BITVECTOR_UREM_TOTAL + || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND + || k == BITVECTOR_OR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR + || k == BITVECTOR_SHL); Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t); TS_ASSERT(!sc.isNull()); @@ -148,7 +148,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite } else { - Assert(idx == 2); + TS_ASSERT(idx == 2); s1 = d_nm->mkVar("s1", d_nm->mkBitVectorType(4)); s2 = d_nm->mkVar("s2", d_nm->mkBitVectorType(4)); x = d_nm->mkBoundVar(s2.getType()); diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index 0b8313222..c0d1474e9 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -21,24 +21,22 @@ #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" #include "expr/type.h" +#include "test_utils.h" using namespace CVC4; using namespace std; class ArrayStoreAllBlack : public CxxTest::TestSuite { ExprManager* d_em; - ExprManagerScope* d_scope; public: void setUp() override { d_em = new ExprManager(); - d_scope = new ExprManagerScope(*d_em); } void tearDown() override { - delete d_scope; delete d_em; } @@ -55,15 +53,15 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite { d_em->mkConst(Rational(0))); } - void testTypeErrors() { - // these two throw an AssertionException in assertions-enabled builds, and - // an IllegalArgumentException in production builds - TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( - d_em->integerType(), - d_em->mkConst(UninterpretedConstant(d_em->mkSort("U"), 0)))); - TS_ASSERT_THROWS_ANYTHING( - ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2)))); - + void testTypeErrors() + { + TS_ASSERT_THROWS(ArrayStoreAll(d_em->integerType(), + d_em->mkConst(UninterpretedConstant( + d_em->mkSort("U"), 0))), + IllegalArgumentException&); + TS_ASSERT_THROWS( + ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))), + IllegalArgumentException&); TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")), d_em->mkConst(Rational(9, 2))), diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index 47acbcc6d..03afcdbf7 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -19,96 +19,49 @@ #include <string> #include <cstring> -#include "base/cvc4_assert.h" +#include "base/check.h" +#include "test_utils.h" using namespace CVC4; using namespace std; class AssertWhite : public CxxTest::TestSuite { public: - - void testAssert() { + void testAssert() + { #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS(Assert(false), AssertionException&); - TS_ASSERT_THROWS(AssertArgument(false, "x"), AssertArgumentException&); + TS_UTILS_EXPECT_ABORT(Assert(false)); + TS_ASSERT_THROWS(AssertArgument(false, "x"), AssertArgumentException&); #else /* CVC4_ASSERTIONS */ - TS_ASSERT_THROWS_NOTHING( Assert(false) ); - TS_ASSERT_THROWS_NOTHING( AssertArgument(false, "x") ); + TS_ASSERT_THROWS_NOTHING(Assert(false)); + TS_ASSERT_THROWS_NOTHING(AssertArgument(false, "x")); #endif /* CVC4_ASSERTIONS */ - TS_ASSERT_THROWS_NOTHING( Assert(true) ); - TS_ASSERT_THROWS(AlwaysAssert(false), AssertionException&); - TS_ASSERT_THROWS(Unreachable(), UnreachableCodeException&); - TS_ASSERT_THROWS(Unhandled(), UnhandledCaseException&); - TS_ASSERT_THROWS(Unimplemented(), UnimplementedOperationException&); - TS_ASSERT_THROWS(IllegalArgument("x"), IllegalArgumentException&); - TS_ASSERT_THROWS(CheckArgument(false, "x"), IllegalArgumentException&); - TS_ASSERT_THROWS(AlwaysAssertArgument(false, "x"), - AssertArgumentException&); - TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") ); - TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") ); - } - - void testReallyLongAssert() { - string msg(1034, 'x'); - try { - AlwaysAssert(false, msg.c_str()); - TS_FAIL("Should have thrown an exception !"); - } catch(AssertionException& e) { - // we don't want to match on the entire string, because it may - // have an absolute path to the unit test binary, line number - // info, etc. - std::string s = e.toString(); - const char* theString = s.c_str(); - const char* firstPart = - "Assertion failure\nvoid AssertWhite::testReallyLongAssert()\n"; - string lastPartStr = "\n\n false\n" + msg; - const char* lastPart = lastPartStr.c_str(); - TS_ASSERT(strncmp(theString, firstPart, strlen(firstPart)) == 0); - TS_ASSERT(strncmp(theString + strlen(theString) - strlen(lastPart), - lastPart, strlen(lastPart)) == 0); - } catch(...) { - TS_FAIL("Threw the wrong kind of exception !"); - } - - // Now test an assert with a format that drives it over the 512 - // byte initial buffer. This was a bug in r1441, see bug: - // https://github.com/CVC4/CVC4/issues/465 - string fmt = string(200, 'x') + " %s " + string(200, 'x'); - string arg(200, 'y'); - try { - AlwaysAssert(false, fmt.c_str(), arg.c_str()); - TS_FAIL("Should have thrown an exception !"); - } catch(AssertionException& e) { - // we don't want to match on the entire string, because it may - // have an absolute path to the unit test binary, line number - // info, etc. - std::string s = e.toString(); - const char* theString = s.c_str(); - const char* firstPart = - "Assertion failure\nvoid AssertWhite::testReallyLongAssert()\n"; - string lastPartStr = "\n\n false\n" + string(200, 'x') + " " + - string(200, 'y') + " " + string(200, 'x'); - const char* lastPart = lastPartStr.c_str(); - TS_ASSERT(strncmp(theString, firstPart, strlen(firstPart)) == 0); - TS_ASSERT(strncmp(theString + strlen(theString) - strlen(lastPart), - lastPart, strlen(lastPart)) == 0); - } catch(...) { - TS_FAIL("Threw the wrong kind of exception !"); - } - } + TS_ASSERT_THROWS_NOTHING(Assert(true)); + TS_UTILS_EXPECT_ABORT(AlwaysAssert(false)); + TS_UTILS_EXPECT_ABORT(Unreachable()); + TS_UTILS_EXPECT_ABORT(Unhandled()); + TS_UTILS_EXPECT_ABORT(Unimplemented()); + TS_ASSERT_THROWS(IllegalArgument("x"), IllegalArgumentException&); + TS_ASSERT_THROWS(CheckArgument(false, "x"), IllegalArgumentException&); + TS_ASSERT_THROWS(AlwaysAssertArgument(false, "x"), AssertArgumentException&); + TS_ASSERT_THROWS_NOTHING(AssertArgument(true, "x")); + TS_ASSERT_THROWS_NOTHING(AssertArgument(true, "x")); + } void testUnreachable() { - TS_ASSERT_THROWS(Unreachable(), UnreachableCodeException&); - TS_ASSERT_THROWS(Unreachable("hello"), UnreachableCodeException&); - TS_ASSERT_THROWS(Unreachable("hello %s", "world"), - UnreachableCodeException&); + TS_UTILS_EXPECT_ABORT(Unreachable()); + TS_UTILS_EXPECT_ABORT(Unreachable() << "hello"); + TS_UTILS_EXPECT_ABORT(Unreachable() << "hello " + << "world"); int x = 5; - TS_ASSERT_THROWS(Unhandled(), UnhandledCaseException&); - TS_ASSERT_THROWS(Unhandled(x), UnhandledCaseException&); - TS_ASSERT_THROWS(Unhandled("foo"), UnhandledCaseException&); - TS_ASSERT_THROWS(Unhandled("foo %s baz", "bar"), UnhandledCaseException&); + TS_UTILS_EXPECT_ABORT(Unhandled()); + TS_UTILS_EXPECT_ABORT(Unhandled() << x); + TS_UTILS_EXPECT_ABORT(Unhandled() << "foo"); + TS_UTILS_EXPECT_ABORT(Unhandled() << "foo " + << "bar" + << " baz"); } }; diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h index 192237b49..3cb18c974 100644 --- a/test/unit/util/binary_heap_black.h +++ b/test/unit/util/binary_heap_black.h @@ -19,6 +19,7 @@ #include <iostream> #include <sstream> +#include "test_utils.h" #include "util/bin_heap.h" using namespace CVC4; @@ -43,8 +44,8 @@ class BinaryHeapBlack : public CxxTest::TestSuite { TS_ASSERT_EQUALS(heap.size(), 0u); TS_ASSERT(heap.empty()); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS_ANYTHING(heap.top()); - TS_ASSERT_THROWS_ANYTHING(heap.pop()); + TS_UTILS_EXPECT_ABORT(heap.top()); + TS_UTILS_EXPECT_ABORT(heap.pop()); #endif /* CVC4_ASSERTIONS */ TS_ASSERT_EQUALS(heap.begin(), heap.end()); @@ -60,8 +61,8 @@ class BinaryHeapBlack : public CxxTest::TestSuite { TS_ASSERT(heap.empty()); TS_ASSERT_EQUALS(heap.size(), 0u); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS_ANYTHING(heap.top()); - TS_ASSERT_THROWS_ANYTHING(heap.pop()); + TS_UTILS_EXPECT_ABORT(heap.top()); + TS_UTILS_EXPECT_ABORT(heap.pop()); #endif /* CVC4_ASSERTIONS */ // Next test a heap of 4 elements @@ -118,8 +119,8 @@ class BinaryHeapBlack : public CxxTest::TestSuite { TS_ASSERT(heap.empty()); TS_ASSERT_EQUALS(heap.size(), 0u); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS_ANYTHING(heap.top()); - TS_ASSERT_THROWS_ANYTHING(heap.pop()); + TS_UTILS_EXPECT_ABORT(heap.top()); + TS_UTILS_EXPECT_ABORT(heap.pop()); #endif /* CVC4_ASSERTIONS */ // Now with a few updates diff --git a/test/unit/util/check_white.h b/test/unit/util/check_white.h index 052a35110..1a169f320 100644 --- a/test/unit/util/check_white.h +++ b/test/unit/util/check_white.h @@ -19,7 +19,7 @@ #include <cstring> #include <string> -#include "base/cvc4_check.h" +#include "base/check.h" #include "test_utils.h" using namespace std; @@ -40,25 +40,25 @@ class CheckWhite : public CxxTest::TestSuite "return type."; } - void testCheck() { CVC4_CHECK(kOne >= 0) << kOne << " must be positive"; } + void testCheck() { AlwaysAssert(kOne >= 0) << kOne << " must be positive"; } void testDCheck() { - CVC4_DCHECK(kOne == 1) << "always passes"; + Assert(kOne == 1) << "always passes"; #ifndef CVC4_ASSERTIONS - CVC4_DCHECK(false) << "Will not be compiled in when CVC4_ASSERTIONS off."; + Assert(false) << "Will not be compiled in when CVC4_ASSERTIONS off."; #endif /* CVC4_ASSERTIONS */ } void testPointerTypeCanBeTheCondition() { const int* one_pointer = &kOne; - CVC4_CHECK(one_pointer); + AlwaysAssert(one_pointer); } void testExpectAbort() { - TS_UTILS_EXPECT_ABORT(CVC4_CHECK(false)); - TS_UTILS_EXPECT_ABORT(CVC4_DCHECK(false)); + TS_UTILS_EXPECT_ABORT(AlwaysAssert(false)); + TS_UTILS_EXPECT_ABORT(Assert(false)); } }; diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index 5cb6c2099..9c40d8a47 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -46,8 +46,8 @@ public: // StatisticsRegistry //static void flushStatistics(std::ostream& out); - //static inline void registerStat(Stat* s) throw (AssertionException); - //static inline void unregisterStat(Stat* s) throw (AssertionException); + // static inline void registerStat(Stat* s); + // static inline void unregisterStat(Stat* s); string empty, bar = "bar", baz = "baz"; ReferenceStat<string> refStr("stat #1", empty); |