Go to the documentation of this file.
9 #ifndef CPROVER_UTIL_INVARIANT_H
10 #define CPROVER_UTIL_INVARIANT_H
16 #include <type_traits>
114 const std::string
function;
123 virtual std::string
what() const noexcept;
126 const std::
string &_file,
127 const std::
string &_function,
129 const std::
string &_backtrace,
130 const std::
string &_condition,
131 const std::
string &_reason)
150 virtual std::string
what() const noexcept;
153 const std::
string &_file,
154 const std::
string &_function,
156 const std::
string &_backtrace,
157 const std::
string &_condition,
158 const std::
string &_reason,
159 const std::
string &_diagnostics)
173 #define CBMC_NORETURN __attribute((noreturn))
174 #elif defined(_MSC_VER)
175 #define CBMC_NORETURN __declspec(noreturn)
176 #elif __cplusplus >= 201703L
177 #define CBMC_NORETURN [[noreturn]]
179 #define CBMC_NORETURN
182 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT)
184 #define INVARIANT(CONDITION, REASON) \
185 __CPROVER_assert((CONDITION), "Invariant : " REASON)
186 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
187 __CPROVER_assert((CONDITION), "Invariant : " REASON)
189 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
190 INVARIANT(CONDITION, "")
192 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK)
197 #define INVARIANT(CONDITION, REASON) \
201 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
205 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false)
207 #elif defined(CPROVER_INVARIANT_ASSERT)
211 #define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true))
212 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
213 assert((CONDITION) && ((REASON), true))
215 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION))
237 template <
class ET,
typename... Params>
239 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
241 const std::string &
file,
242 const std::string &
function,
244 const std::string &condition,
254 std::forward<Params>(params)...);
277 const std::string &
file,
278 const std::string &
function,
280 const std::string &condition,
281 const std::string &reason)
283 invariant_violated_structured<invariant_failedt>(
284 file,
function, line, condition, reason);
289 template <
typename T>
298 template <
typename T>
304 "to avoid unintended strangeness, diagnostics_helpert needs to be "
305 "specialised for each diagnostic type");
312 template <std::
size_t N>
348 template <
typename T>
352 typename std::remove_cv<typename std::remove_reference<T>::type>::type>::
353 diagnostics_as_string(std::forward<T>(val));
360 template <
typename T,
typename... Ts>
367 template <
typename... Diagnostics>
370 std::ostringstream out;
371 out <<
"\n<< EXTRA DIAGNOSTICS >>";
373 out <<
"\n<< END EXTRA DIAGNOSTICS >>";
379 template <
typename... Diagnostics>
381 const std::string &
file,
382 const std::string &
function,
385 std::string condition,
386 Diagnostics &&... diagnostics)
388 invariant_violated_structured<invariant_with_diagnostics_failedt>(
397 #define EXPAND_MACRO(x) x
403 #define CURRENT_FUNCTION_NAME __FUNCTION__
405 #define CURRENT_FUNCTION_NAME __func__
408 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
412 invariant_violated_structured<TYPENAME>( \
414 CURRENT_FUNCTION_NAME, \
424 #define INVARIANT(CONDITION, REASON) \
429 invariant_violated_string( \
430 __FILE__, CURRENT_FUNCTION_NAME, __LINE__, #CONDITION, REASON); \
438 #define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
443 report_invariant_failure( \
445 CURRENT_FUNCTION_NAME, \
453 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block
464 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")
465 #define PRECONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \
466 INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__)
468 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
469 EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
480 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")
481 #define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION, ...) \
482 INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__)
484 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \
485 EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
496 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")
497 #define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION, ...) \
498 INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__)
500 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \
501 EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
504 #define UNREACHABLE INVARIANT(false, "Unreachable")
505 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \
506 EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))
511 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
512 #define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) \
513 INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__)
515 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \
516 EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))
522 #define TODO INVARIANT(false, "Todo")
523 #define UNIMPLEMENTED INVARIANT(false, "Unimplemented")
524 #define UNHANDLED_CASE INVARIANT(false, "Unhandled case")
526 #endif // CPROVER_UTIL_INVARIANT_H
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(std::string string)
std::string assemble_diagnostics()
std::string get_backtrace()
Returns a backtrace.
const std::string condition
void print_backtrace(std::ostream &out)
Prints a back trace to 'out'.
A logic error, augmented with a distinguished field to hold a backtrace.
void report_exception_to_stderr(const invariant_failedt &)
Dump exception report to stderr.
std::string diagnostic_as_string(T &&val)
const std::string diagnostics
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'.
Helper to enable invariant throwing as above bounded to an object lifetime:
~cbmc_invariants_should_throwt()
const std::string backtrace
virtual ~invariant_failedt()=default
bool cbmc_invariants_should_throw
Set this to true to cause invariants to throw a C++ exception rather than abort the program.
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])
A class that includes diagnostic information related to an invariant violation.
void write_rest_diagnostics(std::ostream &)
const std::string function
cbmc_invariants_should_throwt()
static std::string diagnostics_as_string(const T &)
virtual std::string what() const noexcept
virtual std::string what() const noexcept
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)'.