Go to the documentation of this file.
9 #ifndef CPROVER_UTIL_INVARIANT_H
10 #define CPROVER_UTIL_INVARIANT_H
16 #include <type_traits>
92 const std::string
function;
101 virtual std::string
what() const noexcept;
104 const std::
string &_file,
105 const std::
string &_function,
107 const std::
string &_backtrace,
108 const std::
string &_condition,
109 const std::
string &_reason)
128 virtual std::string
what() const noexcept;
131 const std::
string &_file,
132 const std::
string &_function,
134 const std::
string &_backtrace,
135 const std::
string &_condition,
136 const std::
string &_reason,
137 const std::
string &_diagnostics)
151 #define CBMC_NORETURN __attribute((noreturn))
152 #elif defined(_MSV_VER)
153 #define CBMC_NORETURN __declspec(noreturn)
154 #elif __cplusplus >= 201703L
155 #define CBMC_NORETURN [[noreturn]]
157 #define CBMC_NORETURN
160 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
162 #define INVARIANT(CONDITION, REASON) \
163 __CPROVER_assert((CONDITION), "Invariant : " REASON)
164 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
165 __CPROVER_assert((CONDITION), "Invariant : " REASON)
167 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
168 INVARIANT(CONDITION, "")
170 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
175 #define INVARIANT(CONDITION, REASON) \
179 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
183 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false)
185 #elif defined(CPROVER_INVARIANT_ASSERT)
189 #define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true))
190 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
191 assert((CONDITION) && ((REASON), true))
193 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION))
215 template <
class ET,
typename... Params>
217 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
219 const std::string &
file,
220 const std::string &
function,
222 const std::string &condition,
232 std::forward<Params>(params)...);
251 const std::string &
file,
252 const std::string &
function,
254 const std::string &condition,
255 const std::string &reason)
257 invariant_violated_structured<invariant_failedt>(
258 file,
function, line, condition, reason);
263 template <
typename T>
272 template <
typename T>
278 "to avoid unintended strangeness, diagnostics_helpert needs to be "
279 "specialised for each diagnostic type");
286 template <std::
size_t N>
322 template <
typename T>
326 typename std::remove_cv<typename std::remove_reference<T>::type>::type>::
327 diagnostics_as_string(std::forward<T>(val));
334 template <
typename T,
typename... Ts>
341 template <
typename... Diagnostics>
344 std::ostringstream out;
345 out <<
"\n<< EXTRA DIAGNOSTICS >>";
347 out <<
"\n<< END EXTRA DIAGNOSTICS >>";
353 template <
typename... Diagnostics>
355 const std::string &
file,
356 const std::string &
function,
359 std::string condition,
360 Diagnostics &&... diagnostics)
362 invariant_violated_structured<invariant_with_diagnostics_failedt>(
371 #define EXPAND_MACRO(x) x
377 #define CURRENT_FUNCTION_NAME __FUNCTION__
379 #define CURRENT_FUNCTION_NAME __func__
382 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
386 invariant_violated_structured<TYPENAME>( \
388 CURRENT_FUNCTION_NAME, \
394 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
400 #define INVARIANT(CONDITION, REASON) \
405 invariant_violated_string( \
406 __FILE__, CURRENT_FUNCTION_NAME, __LINE__, #CONDITION, REASON); \
414 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
419 report_invariant_failure( \
421 CURRENT_FUNCTION_NAME, \
438 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
439 #define PRECONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \
440 INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__)
442 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
443 EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
454 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
455 #define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \
456 INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__)
458 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
459 EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
470 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
471 #define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION, ...) \
472 INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__)
474 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
475 EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
478 #define UNREACHABLE INVARIANT(false, "Unreachable")
479 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
480 EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))
485 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
486 #define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
487 INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__)
489 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
490 EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
496 #define TODO INVARIANT(false, "Todo")
497 #define UNIMPLEMENTED INVARIANT(false, "Unimplemented")
498 #define UNHANDLED_CASE INVARIANT(false, "Unhandled case")
500 #endif // CPROVER_UTIL_INVARIANT_H
static std::string diagnostics_as_string(std::string string)
std::string assemble_diagnostics()
const std::string condition
void invariant_violated_string(const std::string &file, const std::string &function, const int line, const std::string &condition, const std::string &reason)
This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'.
std::string get_backtrace()
Returns a backtrace.
void report_invariant_failure(const std::string &file, const std::string &function, int line, std::string reason, std::string condition, Diagnostics &&... diagnostics)
This is a wrapper function, used by the macro 'INVARIANT_WITH_DIAGNOSTICS'.
A logic error, augmented with a distinguished field to hold a backtrace.
std::string diagnostic_as_string(T &&val)
const std::string diagnostics
void print_backtrace(std::ostream &out)
Prints a back trace to 'out'.
const std::string backtrace
virtual ~invariant_failedt()=default
std::enable_if< std::is_base_of< invariant_failedt, ET >::value >::type invariant_violated_structured(const std::string &file, const std::string &function, const int line, const std::string &condition, Params &&... params)
This function is the backbone of all the invariant types.
static std::string diagnostics_as_string(const char *string)
Helper to give us some diagnostic in a usable form on assertion failure.
static std::string diagnostics_as_string(const char(&string)[N])
void report_exception_to_stderr(const invariant_failedt &)
Dump exception report to stderr.
A class that includes diagnostic information related to an invariant violation.
void write_rest_diagnostics(std::ostream &)
const std::string function
static std::string diagnostics_as_string(const T &)
virtual std::string what() const noexcept
virtual std::string what() const noexcept