Refactor invariant_failedt definition.

Author: NlightNFotis

src/util/invariant.cpp

@@ -79,8 +79,6 @@ void print_backtrace(
   std::ostream &out)
 {
 #ifdef __GLIBC__
-    out << "Backtrace\n" << std::flush;
-
     void * stack[50] = {};
 
     std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *));
@@ -116,21 +114,14 @@ void report_exception_to_stderr(const invariant_failedt &reason)
   std::cerr << "--- end invariant violation report ---\n";
 }
 
-std::string invariant_failedt::get_invariant_failed_message(
-  const std::string &file,
-  const std::string &function,
-  int line,
-  const std::string &backtrace,
-  const std::string &reason) const
+std::string invariant_failedt::what() const noexcept
 {
   std::ostringstream out;
   out << "Invariant check failed\n"
-      << "File " << file
-      << " function " << function
-      << " line " << line << '\n'
+      << "File: " << file << ":" << line << " function: " << function << '\n'
       << "Condition: " << condition << '\n'
-      << "Reason: " << reason
-      << "\nBacktrace:\n"
+      << "Reason: " << reason << '\n'
+      << "Backtrace:" << '\n'
       << backtrace << '\n';
   return out.str();
 }

src/util/invariant.h

@@ -75,40 +75,29 @@ Author: Martin Brain, [email protected]
 class invariant_failedt
 {
  private:
-   std::string get_invariant_failed_message(
-     const std::string &file,
-     const std::string &function,
-     int line,
-     const std::string &backtrace,
-     const std::string &reason) const;
-
- public:
   const std::string file;
   const std::string function;
   const int line;
   const std::string backtrace;
-  const std::string reason;
   const std::string condition;
+  const std::string reason;
 
-  std::string what() const noexcept
-  {
-    return get_invariant_failed_message(
-      file, function, line, backtrace, reason);
-  };
+public:
+  std::string what() const noexcept;
 
   invariant_failedt(
     const std::string &_file,
     const std::string &_function,
     int _line,
     const std::string &_backtrace,
-    const std::string &_reason,
-    const std::string &_condition)
+    const std::string &_condition,
+    const std::string &_reason)
     : file(_file),
       function(_function),
       line(_line),
       backtrace(_backtrace),
-      reason(_reason),
-      condition(_condition)
+      condition(_condition),
+      reason(_reason)
   {
   }
 };
@@ -171,8 +160,8 @@ invariant_violated_structured(
     function,
     line,
     backtrace,
-    std::forward<Params>(params)...,
-    condition);
+    condition,
+    std::forward<Params>(params)...);
   // We now have a structured exception ready to use;
   // in future this is the place to put a 'throw'.
   report_exception_to_stderr(to_throw);
@@ -230,8 +219,8 @@ invariant_violated_string(
         __FILE__,                                                              \
         __this_function__,                                                     \
         __LINE__,                                                              \
-        __VA_ARGS__,                                                           \
-        #CONDITION); /* NOLINT */                                              \
+        #CONDITION,                                                            \
+        __VA_ARGS__); /* NOLINT */                                             \
   } while(false)
 
 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block