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
Generate Equation using Symbolic Execution.
equation_conversion_exceptiont(const std::string &message, const symex_target_equationt::SSA_stept &step)
symex_target_equationt::SSA_stept step
const char * what() const optional_noexcept override
void output(const namespacet &ns, std::ostream &out) const
static format_containert< T > format(const T &o)
Definition: format.h:35