Invariant with diagnostics

regression/invariants/driver.cpp

@@ -56,6 +56,31 @@ class structured_error_testt: public invariant_failedt
   }
 };
 
+struct DiagnosticA
+{
+};
+struct DiagnosticB
+{
+};
+
+template <>
+struct diagnostics_helpert<DiagnosticA>
+{
+  static std::string diagnostics_as_string(const DiagnosticA &)
+  {
+    return "Diagnostic A";
+  }
+};
+
+template <>
+struct diagnostics_helpert<DiagnosticB>
+{
+  static std::string diagnostics_as_string(const DiagnosticB &)
+  {
+    return "Diagnostic B";
+  }
+};
+
 /// 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.
@@ -118,6 +143,12 @@ int main(int argc, char** argv)
       "diagnostic 2",
       "diagnostic 3",
       "diagnostic 4");
+  else if(arg == "invariant-with-custom-diagnostics")
+    INVARIANT_WITH_DIAGNOSTICS(
+      false,
+      "an invariant with some custom diagnostics",
+      DiagnosticA{},
+      DiagnosticB{});
   else
     return 1;
 }

regression/invariants/invariant-failure19/test.desc

@@ -0,0 +1,11 @@
+CORE
+dummy_parameter.c
+invariant-with-lots-of-diagnostics
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+diagnostic 1
+diagnostic 2
+diagnostic 3
+diagnostic 4

regression/invariants/invariant-failure20/test.desc

@@ -0,0 +1,9 @@
+CORE
+dummy_parameter.c
+invariant-with-custom-diagnostics
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--- begin invariant violation report ---
+Invariant check failed
+Diagnostic A
+Diagnostic B

src/util/invariant.h

@@ -142,11 +142,6 @@ class invariant_with_diagnostics_failedt : public invariant_failedt
 #else
 #define CBMC_NORETURN
 #endif
-// The macros MACRO<n> (e.g., INVARIANT2) are for internal use in this file
-// only. The corresponding macros that take a variable number of arguments (see
-// further below) should be used instead, which in turn call those with a fixed
-// number of arguments. For example, if INVARIANT(...) is called with two
-// arguments, it calls INVARIANT2().
 
 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
 // Used to allow CPROVER to check itself
@@ -321,17 +316,17 @@ inline void write_rest_diagnostics(std::ostream &)
 template <typename T, typename... Ts>
 void write_rest_diagnostics(std::ostream &out, T &&next, Ts &&... rest)
 {
-  out << ", " << diagnostic_as_string(std::forward<T>(next));
+  out << "\n" << diagnostic_as_string(std::forward<T>(next));
   write_rest_diagnostics(out, std::forward<Ts>(rest)...);
 }
 
-template <typename T, typename... Ts>
-std::string assemble_diagnostics(T &&first, Ts &&... rest)
+template <typename... Diagnostics>
+std::string assemble_diagnostics(Diagnostics &&... args)
 {
   std::ostringstream out;
-  out << "[ " << diagnostic_as_string(std::forward<T>(first));
-  write_rest_diagnostics(out, std::forward<Ts>(rest)...);
-  out << " ]";
+  out << "\n<< EXTRA DIAGNOSTICS >>";
+  write_rest_diagnostics(out, std::forward<Diagnostics>(args)...);
+  out << "\n<< END EXTRA DIAGNOSTICS >>";
   return out.str();
 }
 } // namespace detail
@@ -457,18 +452,14 @@ CBMC_NORETURN void report_invariant_failure(
 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...)                      \
   EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
 
-// This should be used to mark dead code
+/// This should be used to mark dead code
 #define UNREACHABLE INVARIANT(false, "Unreachable")
 #define UNREACHABLE_STRUCTURED(TYPENAME, ...)                                  \
   EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))
 
-// This condition should be used to document that assumptions that are
-// made on goto_functions, goto_programs, exprts, etc. being well formed.
-// "The data structure is not corrupt or malformed"
-#define DATA_INVARIANT2(CONDITION, REASON) INVARIANT2(CONDITION, REASON)
-#define DATA_INVARIANT3(CONDITION, REASON, DIAGNOSTICS)                        \
-  INVARIANT3(CONDITION, REASON, DIAGNOSTICS)
-
+/// This condition should be used to document that assumptions that are
+/// made on goto_functions, goto_programs, exprts, etc. being well formed.
+/// "The data structure is not corrupt or malformed"
 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
 #define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...)                \
   INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__)
@@ -482,6 +473,6 @@ CBMC_NORETURN void report_invariant_failure(
 // to migrate documentation and "error handling" in older code.
 #define TODO INVARIANT(false, "Todo")
 #define UNIMPLEMENTED INVARIANT(false, "Unimplemented")
-#define UNHANDLED_CASE INVARIANT2(false, "Unhandled case")
+#define UNHANDLED_CASE INVARIANT(false, "Unhandled case")
 
 #endif // CPROVER_UTIL_INVARIANT_H

src/util/source_location.h

@@ -197,7 +197,7 @@ struct diagnostics_helpert<source_locationt>
   static std::string
   diagnostics_as_string(const source_locationt &source_location)
   {
-    return source_location.as_string();
+    return "source location: " + source_location.as_string();
   }
 };