CBMC
Loading...
Searching...
No Matches
exception_utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Exception helper utilities
4
5Author: 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{
26public:
30 virtual std::string what() const;
31 virtual ~cprover_exception_baset() = default;
32
33protected:
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
58public:
60 std::string reason,
61 std::string option,
62 std::string correct_input = "");
63
64 std::string what() const override;
65};
66
72{
73public:
74 explicit system_exceptiont(std::string message);
75};
76
80{
81public:
82 explicit deserialization_exceptiont(std::string message);
83};
84
92{
93public:
94 explicit incorrect_goto_program_exceptiont(std::string message);
95
96 template <typename Diagnostic, typename... Diagnostics>
98 std::string message,
101
102 template <typename... Diagnostics>
104 std::string message,
107
108 std::string what() const override;
109
110private:
112
113 std::string diagnostics;
114};
115
116template <typename Diagnostic, typename... Diagnostics>
118 std::string message,
120 Diagnostics &&... diagnostics)
121 : cprover_exception_baset(std::move(message)),
122 source_location(source_locationt::nil()),
123 diagnostics(detail::assemble_diagnostics(
125 std::forward<Diagnostics>(diagnostics)...))
126{
127}
128
129template <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{
146public:
148 explicit unsupported_operation_exceptiont(std::string message);
149};
150
154{
155public:
156 explicit analysis_exceptiont(std::string reason);
157};
158
163{
164public:
165 explicit invalid_input_exceptiont(std::string reason);
166};
167
172{
173public:
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
189private:
191};
192
193#endif // CPROVER_UTIL_EXCEPTION_UTILS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Base class for exceptions thrown in the cprover project.
Definition c_errors.h:64
virtual std::string what() const
A human readable description of what went wrong.
virtual ~cprover_exception_baset()=default
cprover_exception_baset(std::string reason)
This constructor is marked protected to ensure this class isn't used directly.
std::string reason
The reason this exception was generated.
Definition c_errors.h:83
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
incorrect_goto_program_exceptiont(std::string message)
std::string what() const override
A human readable description of what went wrong.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
std::string what() const override
A human readable description of what went wrong.
std::string correct_input
In case we have samples of correct input to the option.
std::string option
The full command line option (not the argument) that got erroneous input.
Thrown when user-provided input cannot be processed.
Thrown when we can't handle something in an input source file.
const source_locationt & get_source_location() const
std::string what() const override
A human readable description of what went wrong.
const std::string & get_reason() const
Thrown when some external system fails unexpectedly.
Thrown when we encounter an instruction, parameters to an instruction etc.
STL namespace.