cprover
equation_conversion_exceptions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
13 #define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
14 
15 #include <sstream>
16 
17 #include <util/format_expr.h>
18 
19 #include "symex_target_equation.h"
20 
21 class equation_conversion_exceptiont : public std::runtime_error
22 {
23 public:
25  const std::string &message,
27  : runtime_error(message), step(step)
28  {
29  std::ostringstream error_msg;
30  error_msg << runtime_error::what();
31  error_msg << "\nSource GOTO statement: " << format(step.source.pc->code);
32  error_msg << "\nStep:\n";
33  step.output(error_msg);
34  error_message = error_msg.str();
35  }
36 
37  const char *what() const optional_noexcept override
38  {
39  return error_message.c_str();
40  }
41 
42 private:
44  std::string error_message;
45 };
46 
47 #endif // CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H
equation_conversion_exceptiont::error_message
std::string error_message
Definition: equation_conversion_exceptions.h:44
symex_target_equation.h
format
static format_containert< T > format(const T &o)
Definition: format.h:35
symex_target_equationt::SSA_stept::output
void output(const namespacet &ns, std::ostream &out) const
Definition: symex_target_equation.cpp:729
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:41
symex_target_equationt::SSA_stept
Single SSA step in the equation.
Definition: symex_target_equation.h:243
equation_conversion_exceptiont::what
const char * what() const optional_noexcept override
Definition: equation_conversion_exceptions.h:37
equation_conversion_exceptiont::equation_conversion_exceptiont
equation_conversion_exceptiont(const std::string &message, const symex_target_equationt::SSA_stept &step)
Definition: equation_conversion_exceptions.h:24
symex_target_equationt::SSA_stept::source
sourcet source
Definition: symex_target_equation.h:246
equation_conversion_exceptiont::step
symex_target_equationt::SSA_stept step
Definition: equation_conversion_exceptions.h:43
format_expr.h
equation_conversion_exceptiont
Definition: equation_conversion_exceptions.h:21