test: Add TS_UTILS_EXPECT_ABORT macro for unit tests. (#3378)

TS_UTILS_EXPECT_ABORT can be used if an expression in a unit test is
expected to abort() instead of throwing an exception. This can happen if
CVC4_CHECK or CVC4_DCHECK fail.

2 files changed, 44 insertions, 0 deletions

diff --git a/test/unit/test_utils.h b/test/unit/test_utils.h
new file mode 100644
index 000000000..67bc34456
--- /dev/null
+++ b/test/unit/test_utils.h
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file test_utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Utilities for testing.
+ **
+ **/
+
+#include <sys/wait.h>
+#include <unistd.h>
+
+/**
+ * Use TS_UTILS_EXPECT_ABORT if you expect the expression to abort() when a
+ * CVC4_CHECK or CVC4_DCHECK is triggered.
+ */
+#define TS_UTILS_EXPECT_ABORT(expr) \
+  do                                \
+  {                                 \
+    int32_t status;                 \
+    if (fork())                     \
+    {                               \
+      wait(&status);                \
+    }                               \
+    else                            \
+    {                               \
+      expr;                         \
+      exit(EXIT_SUCCESS);           \
+    }                               \
+    TS_ASSERT(WIFSIGNALED(status)); \
+  } while (0)
diff --git a/test/unit/util/check_white.h b/test/unit/util/check_white.h
index 26a816163..052a35110 100644
--- a/test/unit/util/check_white.h
+++ b/test/unit/util/check_white.h
@@ -20,6 +20,7 @@
 #include <string>
 
 #include "base/cvc4_check.h"
+#include "test_utils.h"
 
 using namespace std;
 using namespace CVC4;
@@ -53,6 +54,12 @@ class CheckWhite : public CxxTest::TestSuite
     const int* one_pointer = &kOne;
     CVC4_CHECK(one_pointer);
   }
+
+  void testExpectAbort()
+  {
+    TS_UTILS_EXPECT_ABORT(CVC4_CHECK(false));
+    TS_UTILS_EXPECT_ABORT(CVC4_DCHECK(false));
+  }
 };
 
 }  // namespace