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" &&
+    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
     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,6 +6,7 @@ DIRS = ansi-c \
        goto-instrument \
        goto-instrument-typedef \
        goto-diff \
+       invariants \
        test-script \
        # Empty last line
 

regression/invariants/.gitignore

@@ -0,0 +1 @@
+driver

regression/invariants/Makefile

@@ -0,0 +1,32 @@
+default: tests.log
+
+SRC = driver.cpp
+
+INCLUDES = -I ../../src
+
+OBJ += ../../src/util/util$(LIBEXT)
+
+include ../../src/config.inc
+include ../../src/common
+
+test: driver$(EXEEXT)
+	@if ! ../test.pl -c ../driver ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl driver$(EXEEXT)
+	@if ! ../test.pl -c ../driver ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+driver$(EXEEXT): $(OBJ)
+	$(LINKBIN)

regression/invariants/driver.cpp

@@ -0,0 +1,88 @@
+/*******************************************************************\
+
+Module: Invariant violation testing
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Invariant violation testing
+
+#include <string>
+#include <sstream>
+#include <util/invariant.h>
+
+/// An example of structured invariants-- this contains fields to
+/// describe the error to a catcher, and also produces a human-readable
+/// message containing all the information for use by the current aborting
+/// invariant implementation and/or any generic error catcher in the future.
+class structured_error_testt: public invariant_failedt
+{
+  std::string pretty_print(int code, const std::string &desc)
+  {
+    std::ostringstream ret;
+    ret << "Error code: " << code
+        << "\nDescription: " << desc;
+    return ret.str();
+  }
+
+public:
+  const int error_code;
+  const std::string description;
+
+  structured_error_testt(
+    const std::string &file,
+    const std::string &function,
+    int line,
+    const std::string &backtrace,
+    int code,
+    const std::string &_description):
+    invariant_failedt(
+      file,
+      function,
+      line,
+      backtrace,
+      pretty_print(code, _description)),
+    error_code(code),
+    description(_description)
+  {
+  }
+};
+
+/// Causes an invariant failure dependent on first argument value.
+/// One ignored argument is accepted to conform with the test.pl script,
+/// which would be the input source file for other cbmc driver programs.
+/// Returns 1 on unexpected arguments.
+int main(int argc, char** argv)
+{
+  if(argc!=3)
+    return 1;
+  std::string arg=argv[1];
+  if(arg=="structured")
+    INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="string")
+    INVARIANT(false, "Test invariant failure");
+  else if(arg=="precondition-structured")
+    PRECONDITION_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="precondition-string")
+    PRECONDITION(false);
+  else if(arg=="postcondition-structured")
+    POSTCONDITION_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="postcondition-string")
+    POSTCONDITION(false);
+  else if(arg=="check-return-structured")
+    CHECK_RETURN_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="check-return-string")
+    CHECK_RETURN(false);
+  else if(arg=="unreachable-structured")
+    UNREACHABLE_STRUCTURED(structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="unreachable-string")
+    UNREACHABLE;
+  else if(arg=="data-invariant-structured")
+    DATA_INVARIANT_STRUCTURED(false, structured_error_testt, 1, "Structured error"); // NOLINT
+  else if(arg=="data-invariant-string")
+    DATA_INVARIANT(false, "Test invariant failure");
+  else
+    return 1;
+}

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

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

regression/invariants/invariant-failure10/test.desc

@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+unreachable-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure11/test.desc

@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+data-invariant-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Test invariant failure
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure12/test.desc

@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+data-invariant-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure2/test.desc

@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure3/test.desc

@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+precondition-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Precondition
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure4/test.desc

@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+precondition-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure5/test.desc

@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+postcondition-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Postcondition
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure6/test.desc

@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+postcondition-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure7/test.desc

@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+check-return-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Check return value
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure8/test.desc

@@ -0,0 +1,13 @@
+CORE
+dummy_parameter.c
+check-return-structured
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Error code: 1
+Description: Structured error
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure9/test.desc

@@ -0,0 +1,12 @@
+CORE
+dummy_parameter.c
+unreachable-string
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Unreachable
+Invariant check failed
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

src/cbmc/cbmc_parse_options.cpp

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