Tests for new invariant macros

Author: danpoe

regression/invariants/driver.cpp

@@ -91,6 +91,22 @@ int main(int argc, char** argv)
     DATA_INVARIANT(false, "Test invariant failure");
   else if(arg=="irep")
     INVARIANT_WITH_IREP(false, "error with irep", pointer_type(void_typet()));
+  else if(arg=="invariant-diagnostics")
+    INVARIANT(
+      false,
+      "invariant with diagnostics failure",
+      "invariant diagnostics information");
+  else if(arg=="precondition-diagnostics")
+    PRECONDITION(false, "precondition diagnostics information");
+  else if(arg=="postcondition-diagnostics")
+    POSTCONDITION(false, "postcondition diagnostics information");
+  else if(arg=="check-return-diagnostics")
+    CHECK_RETURN(false, "check return diagnostics information");
+  else if(arg=="data-invariant-diagnostics")
+    DATA_INVARIANT(
+      false,
+      "data invariant with diagnostics failure",
+      "data invariant diagnostics information");
   else
     return 1;
 }

regression/invariants/invariant-failure14/test.desc

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

regression/invariants/invariant-failure15/test.desc

@@ -0,0 +1,11 @@
+CORE
+dummy_parameter.c
+precondition-diagnostics
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+precondition diagnostics information
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure16/test.desc

@@ -0,0 +1,11 @@
+CORE
+dummy_parameter.c
+postcondition-diagnostics
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+postcondition diagnostics information
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/invariants/invariant-failure17/test.desc

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

regression/invariants/invariant-failure18/test.desc

@@ -0,0 +1,11 @@
+CORE
+dummy_parameter.c
+data-invariant-diagnostics
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+data invariant diagnostics information
+^(Backtrace)|(Backtraces not supported)$
+--
+^warning: ignoring
+^VERIFICATION SUCCESSFUL$