Adjustments to exception printing

Author: thk123

src/goto-symex/symex_target_equation.cpp

@@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/prop/prop.h>
 #include <solvers/prop/literal_expr.h>
 #include <solvers/flattening/bv_conversion_exceptions.h>
+#include <util/string_utils.h>
+#include <util/suffix.h>
 
 #include "goto_symex_state.h"
 #include "equation_conversion_exceptions.h"
@@ -724,24 +726,40 @@ void symex_target_equationt::SSA_stept::output(
   out << "Guard: " << from_expr(ns, "", guard) << '\n';
 }
 
-std::string
-unwrap_exception(const std::exception &e, int level, std::string message)
+/// Given a potentially nested exception, produce a string with all of nested
+/// exceptions information. If a nested exception string contains new lines
+/// then the newlines are indented to the correct level.
+/// \param e: The outer exeception
+/// \param level: How many exceptions have already been unrolled
+/// \return A string with all nested exceptions printed and indented
+std::string unwrap_exception(const std::exception &e, int level)
 {
-  //  messaget message(get_message_handler());
-  //  message.error().source_location=symex.last_source_location;
-  //  message.error() << error_str << messaget::eom;
-  message += std::string(level, ' ') + "exception: " + e.what() + "\n";
+  const std::string msg = e.what();
+  std::vector<std::string> lines;
+  split_string(msg, '\n', lines, false, true);
+  std::ostringstream message_stream;
+  message_stream << std::string(level, ' ') << "exception: ";
+  join_strings(
+    message_stream, lines.begin(), lines.end(), "\n" + std::string(level, ' '));
+
   try
   {
     std::rethrow_if_nested(e);
   }
   catch(const std::exception &e)
   {
-    unwrap_exception(e, level + 1, message);
+    std::string nested_message = unwrap_exception(e, level + 1);
+    // Some exception messages already end in  a new line (e.g. as they have
+    // dumped an irept. Most do not so add a new line on.
+    if(!has_suffix(nested_message, "\n"))
+    {
+      message_stream << '\n';
+    }
+    message_stream << nested_message;
   }
   catch(...)
   {
     UNREACHABLE;
   }
-  return message;
+  return message_stream.str();
 }

src/goto-symex/symex_target_equation.h

@@ -331,17 +331,6 @@ inline bool operator<(
 
 std::string unwrap_exception(
   const std::exception &e,
-  int level = 0,
-  std::string message = "");
-
-class guard_conversion_exceptiont : public std::runtime_error
-{
-public:
-  guard_conversion_exceptiont(const symex_target_equationt::SSA_stept &step) :
-    std::runtime_error("Error converting guard for step"), step(step)
-  {}
-private:
-  symex_target_equationt::SSA_stept step;
-};
+  int level = 0);
 
 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H