Fix irept printing in failed unit tests

regression/CMakeLists.txt

@@ -87,3 +87,5 @@ endif()
 if(NOT WIN32)
   add_subdirectory(crangler)
 endif()
+
+add_subdirectory(catch-framework)

regression/Makefile

@@ -51,6 +51,7 @@ DIRS = cbmc \
        goto-interpreter \
        cbmc-sequentialization \
        cpp-linter \
+       catch-framework \
        # Empty last line
 
 ifeq ($(OS),Windows_NT)

regression/catch-framework/CMakeLists.txt

@@ -0,0 +1,4 @@
+
+add_test_pl_tests(
+    "$<TARGET_FILE:unit>"
+)

regression/catch-framework/Makefile

@@ -0,0 +1,9 @@
+default: test
+
+test:
+	@../test.pl -e -p -c "../../../unit/unit_tests"
+
+tests.log: ../test.pl test
+
+clean:
+	$(RM) tests*.log

regression/catch-framework/irep-printing/test.desc

@@ -0,0 +1,12 @@
+CORE
+[irep_error_printing]
+
+REQUIRE\( foo == bar \)
+key: value
+^EXIT=0$
+^SIGNAL=0$
+--
+\{\?\}
+--
+Test that when unit tests fail on mismatching ireps, the ireps are
+pretty-printed and not printed as catch's default of {?}.

unit/testing-utils/use_catch.h

@@ -39,4 +39,7 @@ Author: Michael Tautschnig
 /// Add to the end of test tags to mark a test that is expected to fail
 #define XFAIL "[.][!shouldfail]"
 
+class irept;
+std::ostream &operator<<(std::ostream &os, const irept &value);
+
 #endif // CPROVER_TESTING_UTILS_USE_CATCH_H

unit/util/irep.cpp

@@ -302,3 +302,16 @@ SCENARIO("irept_memory", "[core][utils][irept]")
     }
   }
 }
+
+// This test is expected to fail so that we can test the error printing of the
+// unit test framework for regressions. It is not included in the [core] or
+// default set of tests, so that the usual output is not polluted with
+// irrelevant error messages.
+TEST_CASE(
+  "Catch2 printing of `irept` for test failures.",
+  "[irep_error_printing]" XFAIL)
+{
+  const irept foo{"foo", irept::named_subt{{"key", irept{"value"}}}, {}};
+  const irept bar{"bar"};
+  REQUIRE(foo == bar);
+}