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 virtual std::string what() const noexcept
A logic error, augmented with a distinguished field to hold a backtrace.
A class that includes diagnostic information related to an invariant violation.
static std::string diagnostics_as_string(std::string string)
void write_rest_diagnostics(std::ostream &)
virtual std::string what() const noexcept
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)'.
void print_backtrace(std::ostream &out)
Prints a back trace to 'out'.
virtual ~invariant_failedt()=default
Helper to give us some diagnostic in a usable form on assertion failure.
const std::string function
static std::string diagnostics_as_string(const T &)
const std::string diagnostics
const std::string backtrace
std::string assemble_diagnostics()
std::string get_backtrace()
Returns a backtrace.
static std::string diagnostics_as_string(const char(&string)[N])
void report_exception_to_stderr(const invariant_failedt &)
Dump exception report to stderr.
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.
std::string diagnostic_as_string(T &&val)
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'.
static std::string diagnostics_as_string(const char *string)