Add unit tests of UNIMPLEMENTED macros

To confirm that the new macro is working as expected.

Author: thomasspriggs

unit/Makefile

@@ -114,6 +114,7 @@ SRC += analyses/ai/ai.cpp \
        util/interval_union.cpp \
        util/irep.cpp \
        util/irep_sharing.cpp \
+       util/invariant.cpp \
        util/json_array.cpp \
        util/json_object.cpp \
        util/lazy.cpp \

unit/util/invariant.cpp

@@ -0,0 +1,26 @@
+// Author: Diffblue Ltd.
+
+/// \file Tests for macros in src/util/invariant.h
+
+#include <testing-utils/invariant.h>
+#include <testing-utils/use_catch.h>
+
+#include <util/invariant.h>
+
+TEST_CASE("Using the UNIMPLEMENTED macro", "[invariant]")
+{
+  cbmc_invariants_should_throwt invariants_throw;
+  REQUIRE_THROWS_MATCHES(
+    []() { UNIMPLEMENTED; }(),
+    invariant_failedt,
+    invariant_failure_containing("Reason: Unimplemented"));
+}
+
+TEST_CASE("Using the UNIMPLEMENTED_FEATURE macro", "[invariant]")
+{
+  cbmc_invariants_should_throwt invariants_throw;
+  REQUIRE_THROWS_MATCHES(
+    []() { UNIMPLEMENTED_FEATURE("example"); }(),
+    invariant_failedt,
+    invariant_failure_containing("Reason: Reached unimplemented example"));
+}