Skip to content

Commit 03ec4b0

Browse files
author
thk123
committed
Move unwrap code into util
1 parent 5a57834 commit 03ec4b0

File tree

4 files changed

+74
-40
lines changed

4 files changed

+74
-40
lines changed

src/goto-symex/symex_target_equation.cpp

+1-38
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "symex_target_equation.h"
1313

1414
#include <util/std_expr.h>
15+
#include <util/unwrap_nested_exception.h>
1516

1617
#include <langapi/language_util.h>
1718
#include <solvers/prop/prop_conv.h>
@@ -723,41 +724,3 @@ void symex_target_equationt::SSA_stept::output(
723724

724725
out << "Guard: " << from_expr(ns, "", guard) << '\n';
725726
}
726-
727-
/// Given a potentially nested exception, produce a string with all of nested
728-
/// exceptions information. If a nested exception string contains new lines
729-
/// then the newlines are indented to the correct level.
730-
/// \param e: The outer exeception
731-
/// \param level: How many exceptions have already been unrolled
732-
/// \return A string with all nested exceptions printed and indented
733-
std::string unwrap_exception(const std::exception &e, int level)
734-
{
735-
const std::string msg = e.what();
736-
std::vector<std::string> lines;
737-
split_string(msg, '\n', lines, false, true);
738-
std::ostringstream message_stream;
739-
message_stream << std::string(level, ' ') << "exception: ";
740-
join_strings(
741-
message_stream, lines.begin(), lines.end(), "\n" + std::string(level, ' '));
742-
743-
try
744-
{
745-
std::rethrow_if_nested(e);
746-
}
747-
catch(const std::exception &e)
748-
{
749-
std::string nested_message = unwrap_exception(e, level + 1);
750-
// Some exception messages already end in a new line (e.g. as they have
751-
// dumped an irept. Most do not so add a new line on.
752-
if(!has_suffix(nested_message, "\n"))
753-
{
754-
message_stream << '\n';
755-
}
756-
message_stream << nested_message;
757-
}
758-
catch(...)
759-
{
760-
UNREACHABLE;
761-
}
762-
return message_stream.str();
763-
}

src/goto-symex/symex_target_equation.h

-2
Original file line numberDiff line numberDiff line change
@@ -329,6 +329,4 @@ inline bool operator<(
329329
return &(*a)<&(*b);
330330
}
331331

332-
std::string unwrap_exception(const std::exception &e, int level = 0);
333-
334332
#endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H

src/util/unwrap_nested_exception.cpp

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
/*******************************************************************\
2+
3+
Module: util
4+
5+
Author: Diffblue Ltd.
6+
7+
\*******************************************************************/
8+
9+
#include "unwrap_nested_exception.h"
10+
#include "suffix.h"
11+
12+
#include <string>
13+
#include <exception>
14+
#include <vector>
15+
16+
#include <util/invariant.h>
17+
#include <util/string_utils.h>
18+
#include <sstream>
19+
20+
/// Given a potentially nested exception, produce a string with all of nested
21+
/// exceptions information. If a nested exception string contains new lines
22+
/// then the newlines are indented to the correct level.
23+
/// \param e: The outer exeception
24+
/// \param level: How many exceptions have already been unrolled
25+
/// \return A string with all nested exceptions printed and indented
26+
std::string unwrap_exception(const std::exception &e, int level)
27+
{
28+
const std::string msg = e.what();
29+
std::vector<std::string> lines;
30+
split_string(msg, '\n', lines, false, true);
31+
std::ostringstream message_stream;
32+
message_stream << std::string(level, ' ') << "exception: ";
33+
join_strings(
34+
message_stream, lines.begin(), lines.end(), "\n" + std::string(level, ' '));
35+
36+
try
37+
{
38+
std::rethrow_if_nested(e);
39+
}
40+
catch(const std::exception &e)
41+
{
42+
std::string nested_message = unwrap_exception(e, level + 1);
43+
// Some exception messages already end in a new line (e.g. as they have
44+
// dumped an irept. Most do not so add a new line on.
45+
if(!has_suffix(nested_message, "\n")) // TODO: replace with more C++ style
46+
{
47+
message_stream << '\n';
48+
}
49+
message_stream << nested_message;
50+
}
51+
catch(...)
52+
{
53+
UNREACHABLE;
54+
}
55+
return message_stream.str();
56+
}

src/util/unwrap_nested_exception.h

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
/*******************************************************************\
2+
3+
Module: util
4+
5+
Author: Diffblue Ltd.
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H
10+
#define CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H
11+
12+
#include <string>
13+
#include <exception>
14+
15+
std::string unwrap_exception(const std::exception &e, int level = 0);
16+
17+
#endif // CPROVER_UTIL_UNWRAP_NESTED_EXCEPTION_H

0 commit comments

Comments
 (0)