CBMC
exception_utils.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Exception helper utilities
4 
5 Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_EXCEPTION_UTILS_H
10 #define CPROVER_UTIL_EXCEPTION_UTILS_H
11 
12 #include <string>
13 
14 #include "invariant.h"
15 #include "source_location.h"
16 
25 {
26 public:
30  virtual std::string what() const;
31  virtual ~cprover_exception_baset() = default;
32 
33 protected:
37  explicit cprover_exception_baset(std::string reason)
38  : reason(std::move(reason))
39  {
40  }
41 
44  std::string reason;
45 };
46 
51 {
54  std::string option;
56  std::string correct_input;
57 
58 public:
60  std::string reason,
61  std::string option,
62  std::string correct_input = "");
63 
64  std::string what() const override;
65 };
66 
72 {
73 public:
74  explicit system_exceptiont(std::string message);
75 };
76 
80 {
81 public:
82  explicit deserialization_exceptiont(std::string message);
83 };
84 
92 {
93 public:
94  explicit incorrect_goto_program_exceptiont(std::string message);
95 
96  template <typename Diagnostic, typename... Diagnostics>
98  std::string message,
99  Diagnostic &&diagnostic,
100  Diagnostics &&... diagnostics);
101 
102  template <typename... Diagnostics>
104  std::string message,
106  Diagnostics &&... diagnostics);
107 
108  std::string what() const override;
109 
110 private:
112 
113  std::string diagnostics;
114 };
115 
116 template <typename Diagnostic, typename... Diagnostics>
118  std::string message,
119  Diagnostic &&diagnostic,
120  Diagnostics &&... diagnostics)
121  : cprover_exception_baset(std::move(message)),
122  source_location(source_locationt::nil()),
123  diagnostics(detail::assemble_diagnostics(
124  std::forward<Diagnostic>(diagnostic),
125  std::forward<Diagnostics>(diagnostics)...))
126 {
127 }
128 
129 template <typename... Diagnostics>
131  std::string message,
132  source_locationt source_location,
133  Diagnostics &&... diagnostics)
134  : cprover_exception_baset(std::move(message)),
135  source_location(std::move(source_location)),
136  diagnostics(
137  detail::assemble_diagnostics(std::forward<Diagnostics>(diagnostics)...))
138 {
139 }
140 
145 {
146 public:
148  explicit unsupported_operation_exceptiont(std::string message);
149 };
150 
154 {
155 public:
156  explicit analysis_exceptiont(std::string reason);
157 };
158 
163 {
164 public:
165  explicit invalid_input_exceptiont(std::string reason);
166 };
167 
172 {
173 public:
175  std::string reason,
177  std::string what() const override;
178 
179  const std::string &get_reason() const
180  {
181  return reason;
182  }
183 
185  {
186  return source_location;
187  }
188 
189 private:
191 };
192 
193 #endif // CPROVER_UTIL_EXCEPTION_UTILS_H
detail::assemble_diagnostics
std::string assemble_diagnostics()
Definition: invariant.h:342
cprover_exception_baset::cprover_exception_baset
cprover_exception_baset(std::string reason)
This constructor is marked protected to ensure this class isn't used directly.
Definition: exception_utils.h:37
invalid_source_file_exceptiont::source_location
source_locationt source_location
Definition: exception_utils.h:190
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:79
deserialization_exceptiont::deserialization_exceptiont
deserialization_exceptiont(std::string message)
Definition: exception_utils.cpp:47
unsupported_operation_exceptiont
Thrown when we encounter an instruction, parameters to an instruction etc.
Definition: exception_utils.h:144
invalid_source_file_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: exception_utils.cpp:96
invalid_input_exceptiont
Thrown when user-provided input cannot be processed.
Definition: exception_utils.h:162
invariant.h
incorrect_goto_program_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: exception_utils.cpp:59
detail
Definition: type_traits.h:13
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
invalid_source_file_exceptiont::get_source_location
const source_locationt & get_source_location() const
Definition: exception_utils.h:184
incorrect_goto_program_exceptiont
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Definition: exception_utils.h:91
invalid_command_line_argument_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: exception_utils.cpp:17
incorrect_goto_program_exceptiont::diagnostics
std::string diagnostics
Definition: exception_utils.h:113
system_exceptiont
Thrown when some external system fails unexpectedly.
Definition: exception_utils.h:71
source_location.h
invalid_input_exceptiont::invalid_input_exceptiont
invalid_input_exceptiont(std::string reason)
Definition: exception_utils.cpp:83
incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont
incorrect_goto_program_exceptiont(std::string message)
Definition: exception_utils.cpp:52
analysis_exceptiont::analysis_exceptiont
analysis_exceptiont(std::string reason)
Definition: exception_utils.cpp:78
source_locationt
Definition: source_location.h:18
invalid_source_file_exceptiont::invalid_source_file_exceptiont
invalid_source_file_exceptiont(std::string reason, source_locationt source_location)
Definition: exception_utils.cpp:88
incorrect_goto_program_exceptiont::source_location
source_locationt source_location
Definition: exception_utils.h:111
unsupported_operation_exceptiont::unsupported_operation_exceptiont
unsupported_operation_exceptiont(std::string message)
message is the unsupported operation causing this fault to occur.
Definition: exception_utils.cpp:72
cprover_exception_baset::what
virtual std::string what() const
A human readable description of what went wrong.
Definition: exception_utils.cpp:12
invalid_command_line_argument_exceptiont::invalid_command_line_argument_exceptiont
invalid_command_line_argument_exceptiont(std::string reason, std::string option, std::string correct_input="")
Definition: exception_utils.cpp:32
invalid_command_line_argument_exceptiont::option
std::string option
The full command line option (not the argument) that got erroneous input.
Definition: exception_utils.h:54
invalid_source_file_exceptiont::get_reason
const std::string & get_reason() const
Definition: exception_utils.h:179
system_exceptiont::system_exceptiont
system_exceptiont(std::string message)
Definition: exception_utils.cpp:42
invalid_command_line_argument_exceptiont::correct_input
std::string correct_input
In case we have samples of correct input to the option.
Definition: exception_utils.h:56
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:50
cprover_exception_baset::reason
std::string reason
The reason this exception was generated.
Definition: exception_utils.h:44
cprover_exception_baset::~cprover_exception_baset
virtual ~cprover_exception_baset()=default
cprover_exception_baset
Base class for exceptions thrown in the cprover project.
Definition: exception_utils.h:24
analysis_exceptiont
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Definition: exception_utils.h:153