Move unwrap code into util

Author: thk123

src/goto-symex/symex_target_equation.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "symex_target_equation.h"
 
 #include <util/std_expr.h>
+#include <util/unwrap_nested_exception.h>
 
 #include <langapi/language_util.h>
 #include <solvers/prop/prop_conv.h>
@@ -725,41 +726,3 @@ void symex_target_equationt::SSA_stept::output(
 
   out << "Guard: " << from_expr(ns, "", guard) << '\n';
 }
-
-/// 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)
-{
-  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)
-  {
-    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_stream.str();
-}

src/goto-symex/symex_target_equation.h

@@ -329,8 +329,6 @@ inline bool operator<(
   return &(*a)<&(*b);
 }
 
-std::string unwrap_exception(
-  const std::exception &e,
-  int level = 0);
+
 
 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H

src/util/unwrap_nested_exception.cpp

@@ -0,0 +1,56 @@
+/*******************************************************************\
+
+Module: util
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include "unwrap_nested_exception.h"
+#include "suffix.h"
+
+#include <string>
+#include <exception>
+#include <vector>
+
+#include <util/invariant.h>
+#include <util/string_utils.h>
+#include <sstream>
+
+/// 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)
+{
+  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)
+  {
+    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")) // TODO: replace with more C++ style
+    {
+      message_stream << '\n';
+    }
+    message_stream << nested_message;
+  }
+  catch(...)
+  {
+    UNREACHABLE;
+  }
+  return message_stream.str();
+}

src/util/unwrap_nested_exception.h

@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module: util
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H
+#define CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H
+
+#include <string>
+#include <exception>
+
+std::string unwrap_exception(
+  const std::exception &e,
+  int level = 0);
+
+#endif //CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H