Skip to content

Commit c7fb551

Browse files
committed
Move equation conversion exception to exception utils
1 parent 112bd5b commit c7fb551

File tree

3 files changed

+33
-48
lines changed

3 files changed

+33
-48
lines changed

src/goto-symex/equation_conversion_exceptions.h

-47
This file was deleted.

src/goto-symex/symex_target_equation.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/std_expr.h>
1616
#include <util/throw_with_nested.h>
1717
#include <util/unwrap_nested_exception.h>
18+
#include <util/exception_utils.h>
1819

1920
// Can be removed once deprecated SSA_stept::output is removed
2021
#include <langapi/language_util.h>
@@ -24,7 +25,6 @@ Author: Daniel Kroening, [email protected]
2425
#include <solvers/prop/prop.h>
2526
#include <solvers/prop/prop_conv.h>
2627

27-
#include "equation_conversion_exceptions.h"
2828
#include "goto_symex_state.h"
2929

3030
/// read from a shared variable

src/util/exception_utils.h

+32
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,11 @@ Author: Fotis Koutoulakis, [email protected]
1010
#define CPROVER_UTIL_EXCEPTION_UTILS_H
1111

1212
#include <string>
13+
#include <sstream>
14+
15+
#include <goto-symex/symex_target_equation.h>
16+
17+
#include "format_expr.h"
1318

1419
class invalid_user_input_exceptiont
1520
{
@@ -38,4 +43,31 @@ class invalid_user_input_exceptiont
3843
}
3944
};
4045

46+
47+
class equation_conversion_exceptiont : public std::runtime_error
48+
{
49+
public:
50+
equation_conversion_exceptiont(
51+
const std::string &message,
52+
const symex_target_equationt::SSA_stept &step)
53+
: runtime_error(message), step(step)
54+
{
55+
std::ostringstream error_msg;
56+
error_msg << runtime_error::what();
57+
error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
58+
error_msg << "\nStep:\n";
59+
step.output(error_msg);
60+
error_message = error_msg.str();
61+
}
62+
63+
const char *what() const optional_noexcept override
64+
{
65+
return error_message.c_str();
66+
}
67+
68+
private:
69+
symex_target_equationt::SSA_stept step;
70+
std::string error_message;
71+
};
72+
4173
#endif // CPROVER_UTIL_EXCEPTION_UTILS_H

0 commit comments

Comments
 (0)