Revert "Improved invariants"

.travis.yml

@@ -159,7 +159,7 @@ install:
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
+    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
     eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
     eval ${PRE_COMMAND} ${COMMAND}

regression/Makefile

@@ -6,7 +6,6 @@ DIRS = ansi-c \
        goto-instrument \
        goto-instrument-typedef \
        goto-diff \
-       invariants \
        test-script \
        # Empty last line
 

regression/cbmc/invariant-failure/main.c

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

regression/invariants/invariant-failure/test.desc → regression/cbmc/invariant-failure/test.desc

@@ -1,10 +1,8 @@
 CORE
-dummy_parameter.c
-string
+main.c
+--test-invariant-failure
 ^EXIT=(0|127|134|137)$
 ^SIGNAL=0$
---- begin invariant violation report ---
-Test invariant failure
 Invariant check failed
 ^(Backtrace)|(Backtraces not supported)$
 --

src/cbmc/cbmc_parse_options.cpp

@@ -106,6 +106,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: