Merge pull request #5085 from thomasspriggs/tas/invariant_matcher

Improve catch support for checking of thrown instances of `invariant_failedt`

Author: thomasspriggs

jbmc/unit/java_bytecode/java_string_literals.cpp

@@ -11,6 +11,7 @@ Author: Diffblue Limited
 #include <java_bytecode/java_types.h>
 #include <java_bytecode/java_utils.h>
 #include <linking/static_lifetime_init.h>
+#include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
 #include <util/symbol_table.h>
 
@@ -29,21 +30,10 @@ TEST_CASE(
 
   create_java_initialize(symbol_table);
   symbol_table.get_writeable_ref(INITIALIZE_FUNCTION).value = code_blockt{};
-  try
-  {
-    const cbmc_invariants_should_throwt invariants_throw;
-    get_or_create_string_literal_symbol("bar", symbol_table, false);
-    FAIL("Expected invariant failure.");
-  }
-  catch(const invariant_failedt &exception)
-  {
-    REQUIRE_THAT(
-      exception.what(),
-      Catch::Matchers::Contains("Cannot create more string literals after "
-                                "making " INITIALIZE_FUNCTION));
-  }
-  catch(...)
-  {
-    FAIL("Incorrect exception type thrown.");
-  }
+  const cbmc_invariants_should_throwt invariants_throw;
+  REQUIRE_THROWS_MATCHES(
+    get_or_create_string_literal_symbol("bar", symbol_table, false),
+    invariant_failedt,
+    invariant_failure_containing("Cannot create more string literals after "
+                                 "making " INITIALIZE_FUNCTION));
 }

unit/goto-programs/remove_returns.cpp

@@ -6,6 +6,7 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
+#include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
 
 #include <goto-programs/goto_functions.h>
@@ -52,21 +53,10 @@ TEST_CASE(
       symbol_exprt{"local_variable", signedbv_typet{32}},
       symbol_exprt{"bar_function", code_typet{{}, signedbv_typet{32}}},
       {}});
-  try
-  {
-    const cbmc_invariants_should_throwt invariants_throw;
-    remove_returns(symbol_table, goto_functions);
-    FAIL("Expected invariant failure.");
-  }
-  catch(const invariant_failedt &exception)
-  {
-    REQUIRE_THAT(
-      exception.what(),
-      Catch::Matchers::Contains("called function `bar_function' should have an "
-                                "entry in the function map"));
-  }
-  catch(...)
-  {
-    FAIL("Incorrect exception type thrown.");
-  }
+  const cbmc_invariants_should_throwt invariants_throw;
+  REQUIRE_THROWS_MATCHES(
+    remove_returns(symbol_table, goto_functions),
+    invariant_failedt,
+    invariant_failure_containing("called function `bar_function' should have "
+                                 "an entry in the function map"));
 }

unit/testing-utils/Makefile

@@ -1,6 +1,7 @@
 SRC = \
   call_graph_test_utils.cpp \
   free_form_cmdline.cpp \
+  invariant.cpp \
   message.cpp \
   require_expr.cpp \
   require_symbol.cpp \

unit/testing-utils/invariant.cpp

@@ -0,0 +1,37 @@
+/// Author: Diffblue Ltd.
+
+#include "invariant.h"
+
+#include <utility>
+
+invariant_failure_containingt invariant_failure_containing(std::string expected)
+{
+  return invariant_failure_containingt{std::move(expected)};
+}
+
+invariant_failure_containingt::invariant_failure_containingt(
+  std::string expected)
+  : expected{std::move(expected)}
+{
+}
+
+bool invariant_failure_containingt::match(
+  const invariant_failedt &exception) const
+{
+  const std::string what = exception.what();
+  return what.find(expected) != std::string::npos;
+}
+
+std::string invariant_failure_containingt::describe() const
+{
+  return std::string{"invariant_failedt with `.what' containing - \""} +
+         expected + "\"";
+}
+
+std::ostream &
+operator<<(std::ostream &out, const invariant_failedt &invariant_failed)
+{
+  out << "invariant_failedt where `.what()' is \"" << invariant_failed.what()
+      << "\"";
+  return out;
+}

unit/testing-utils/invariant.h

@@ -0,0 +1,32 @@
+/// Author: Diffblue Ltd.
+
+#ifndef CPROVER_TESTING_UTILS_INVARIANT_H
+#define CPROVER_TESTING_UTILS_INVARIANT_H
+
+#include <testing-utils/use_catch.h>
+#include <util/invariant.h>
+
+#include <string>
+
+class invariant_failure_containingt
+  : public Catch::MatcherBase<invariant_failedt>
+{
+public:
+  explicit invariant_failure_containingt(std::string expected);
+  bool match(const invariant_failedt &exception) const override;
+  std::string describe() const override;
+
+private:
+  std::string expected;
+};
+
+/// Returns a matcher which matches an invariant_failedt exception, where the
+/// `.what()` returns a string containing \p expected.
+invariant_failure_containingt
+invariant_failure_containing(std::string expected);
+
+/// Printing of `invariant_failedt` for test failure messages.
+std::ostream &
+operator<<(std::ostream &out, const invariant_failedt &invariant_failed);
+
+#endif // CPROVER_TESTING_UTILS_INVARIANT_H

unit/util/symbol_table.cpp

@@ -2,6 +2,7 @@
 
 /// \file Tests for symbol_tablet
 
+#include <testing-utils/invariant.h>
 #include <testing-utils/use_catch.h>
 #include <util/exception_utils.h>
 #include <util/journalling_symbol_table.h>
@@ -359,19 +360,8 @@ TEST_CASE("symbol_tablet::lookup_ref invariant", "[core][utils][symbol_tablet]")
   symbol_table.insert(foo_symbol);
   const cbmc_invariants_should_throwt invariants_throw;
   REQUIRE_NOTHROW(symbol_table.lookup_ref("foo"));
-  try
-  {
-    symbol_table.lookup_ref("bar");
-    FAIL("Expected invariant failure.");
-  }
-  catch(const invariant_failedt &exception)
-  {
-    REQUIRE_THAT(
-      exception.what(),
-      Catch::Matchers::Contains("`bar' must exist in the symbol table."));
-  }
-  catch(...)
-  {
-    FAIL("Incorrect exception type thrown.");
-  }
+  REQUIRE_THROWS_MATCHES(
+    symbol_table.lookup_ref("bar"),
+    invariant_failedt,
+    invariant_failure_containing("`bar' must exist in the symbol table."));
 }