Merge pull request #6152 from thomasspriggs/tas/unimplemented_feature

Add  UNIMPLEMENTED_FEATURE macro

Author: thomasspriggs

src/util/invariant.h

@@ -514,6 +514,9 @@ CBMC_NORETURN void report_invariant_failure(
 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...)                    \
   EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
 
+#define UNIMPLEMENTED_FEATURE(FEATURE)                                         \
+  INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))
+
 // Legacy annotations
 
 // The following should not be used in new code and are only intended

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"));
+}