Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

5 files changed, 55 insertions, 103 deletions

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);