Add an (undocumented) option to test out what happens if an invariant fails.

Author: martin

regression/cbmc/invariant-failure/main.c

@@ -0,0 +1,4 @@
+int main()
+{
+  return 0;
+}

regression/cbmc/invariant-failure/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--test-invariant-failure
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

src/cbmc/cbmc_parse_options.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/language.h>
 #include <util/unicode.h>
 #include <util/memory_info.h>
+#include <util/invariant.h>
 
 #include <ansi-c/c_preprocess.h>
 
@@ -104,6 +105,27 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     exit(1); // should contemplate EX_USAGE from sysexits.h
   }
 
+  // Test only; do not use for input validation
+  if(cmdline.isset("test-invariant-failure"))
+  {
+    // Have to catch this as the default handling of uncaught exceptions
+    // on windows appears to be silent termination.
+    try
+    {
+      INVARIANT(0, "Test invariant failure");
+    }
+    catch (const invariant_failedt &e)
+    {
+      std::cerr << e.what();
+      exit(0); // should contemplate EX_OK from sysexits.h
+    }
+    catch (...)
+    {
+      error() << "Unexpected exception type\n";
+    }
+    exit(1);
+  }
+
   if(cmdline.isset("program-only"))
     options.set_option("program-only", true);
 

src/cbmc/cbmc_parse_options.h

@@ -63,6 +63,7 @@ class optionst;
   "(java-cp-include-files):" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \
+  "(test-invariant-failure)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 
 class cbmc_parse_optionst: