cprover
|
#include <cstdlib>
#include <sstream>
#include <stdexcept>
#include <string>
#include <type_traits>
Go to the source code of this file.
Classes | |
class | invariant_failedt |
A logic error, augmented with a distinguished field to hold a backtrace. More... | |
class | invariant_with_diagnostics_failedt |
A class that includes diagnostic information related to an invariant violation. More... | |
struct | detail::always_falset< T > |
struct | diagnostics_helpert< T > |
Helper to give us some diagnostic in a usable form on assertion failure. More... | |
struct | diagnostics_helpert< char[N]> |
struct | diagnostics_helpert< char * > |
struct | diagnostics_helpert< std::string > |
Namespaces | |
detail | |
Macros | |
#define | CBMC_NORETURN |
#define | EXPAND_MACRO(x) x |
#define | CURRENT_FUNCTION_NAME __func__ |
#define | INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) |
#define | INVARIANT(CONDITION, REASON) |
This macro uses the wrapper function 'invariant_violated_string'. More... | |
#define | INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) |
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a specialisation for invariant_helpert This macro uses the wrapper function 'report_invariant_failure'. More... | |
#define | PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition") |
#define | PRECONDITION_WITH_DIAGNOSTICS(CONDITION, ...) INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__) |
#define | PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) |
#define | POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition") |
#define | POSTCONDITION_WITH_DIAGNOSTICS(CONDITION, ...) INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__) |
#define | POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) |
#define | CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value") |
#define | CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION, ...) INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__) |
#define | CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) |
#define | UNREACHABLE INVARIANT(false, "Unreachable") |
This should be used to mark dead code. More... | |
#define | UNREACHABLE_STRUCTURED(TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)) |
#define | DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON) |
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc. More... | |
#define | DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__) |
#define | DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) |
#define | TODO INVARIANT(false, "Todo") |
#define | UNIMPLEMENTED INVARIANT(false, "Unimplemented") |
#define | UNHANDLED_CASE INVARIANT(false, "Unhandled case") |
Functions | |
void | print_backtrace (std::ostream &out) |
Prints a back trace to 'out'. More... | |
std::string | get_backtrace () |
Returns a backtrace. More... | |
void | report_exception_to_stderr (const invariant_failedt &) |
Dump exception report to stderr. More... | |
template<class ET , typename... Params> | |
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. More... | |
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)'. More... | |
std::string | detail::assemble_diagnostics () |
template<typename T > | |
std::string | detail::diagnostic_as_string (T &&val) |
void | detail::write_rest_diagnostics (std::ostream &) |
template<typename T , typename... Ts> | |
void | detail::write_rest_diagnostics (std::ostream &out, T &&next, Ts &&... rest) |
template<typename... Diagnostics> | |
std::string | detail::assemble_diagnostics (Diagnostics &&... args) |
template<typename... 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'. More... | |
#define CBMC_NORETURN |
Definition at line 157 of file invariant.h.
#define CHECK_RETURN | ( | CONDITION | ) | INVARIANT(CONDITION, "Check return value") |
Definition at line 470 of file invariant.h.
#define CHECK_RETURN_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) |
Definition at line 474 of file invariant.h.
#define CHECK_RETURN_WITH_DIAGNOSTICS | ( | CONDITION, | |
... | |||
) | INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__) |
Definition at line 471 of file invariant.h.
#define CURRENT_FUNCTION_NAME __func__ |
Definition at line 379 of file invariant.h.
#define DATA_INVARIANT | ( | CONDITION, | |
REASON | |||
) | INVARIANT(CONDITION, REASON) |
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
being well formed. "The data structure is not corrupt or malformed"
Definition at line 485 of file invariant.h.
#define DATA_INVARIANT_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) |
Definition at line 489 of file invariant.h.
#define DATA_INVARIANT_WITH_DIAGNOSTICS | ( | CONDITION, | |
REASON, | |||
... | |||
) | INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__) |
Definition at line 486 of file invariant.h.
#define EXPAND_MACRO | ( | x | ) | x |
Definition at line 371 of file invariant.h.
#define INVARIANT | ( | CONDITION, | |
REASON | |||
) |
This macro uses the wrapper function 'invariant_violated_string'.
Definition at line 400 of file invariant.h.
#define INVARIANT_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) |
Definition at line 382 of file invariant.h.
#define INVARIANT_WITH_DIAGNOSTICS | ( | CONDITION, | |
REASON, | |||
... | |||
) |
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a specialisation for invariant_helpert This macro uses the wrapper function 'report_invariant_failure'.
Definition at line 414 of file invariant.h.
#define POSTCONDITION | ( | CONDITION | ) | INVARIANT(CONDITION, "Postcondition") |
Definition at line 454 of file invariant.h.
#define POSTCONDITION_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) |
Definition at line 458 of file invariant.h.
#define POSTCONDITION_WITH_DIAGNOSTICS | ( | CONDITION, | |
... | |||
) | INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__) |
Definition at line 455 of file invariant.h.
#define PRECONDITION | ( | CONDITION | ) | INVARIANT(CONDITION, "Precondition") |
Definition at line 438 of file invariant.h.
#define PRECONDITION_STRUCTURED | ( | CONDITION, | |
TYPENAME, | |||
... | |||
) | EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__)) |
Definition at line 442 of file invariant.h.
#define PRECONDITION_WITH_DIAGNOSTICS | ( | CONDITION, | |
... | |||
) | INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__) |
Definition at line 439 of file invariant.h.
#define TODO INVARIANT(false, "Todo") |
Definition at line 496 of file invariant.h.
#define UNHANDLED_CASE INVARIANT(false, "Unhandled case") |
Definition at line 498 of file invariant.h.
#define UNIMPLEMENTED INVARIANT(false, "Unimplemented") |
Definition at line 497 of file invariant.h.
#define UNREACHABLE INVARIANT(false, "Unreachable") |
This should be used to mark dead code.
Definition at line 478 of file invariant.h.
#define UNREACHABLE_STRUCTURED | ( | TYPENAME, | |
... | |||
) | EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__)) |
Definition at line 479 of file invariant.h.
std::string get_backtrace | ( | ) |
Returns a backtrace.
Definition at line 102 of file invariant.cpp.
|
inline |
This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'.
It constructs an invariant_violatedt from reason and the backtrace, then aborts after printing the invariant's description. In future this may throw rather than aborting.
file | : C string giving the name of the file. |
function | : C string giving the name of the function. |
line | : The line number of the invariant |
reason | : brief description of the invariant violation. |
condition | : the condition this invariant is checking. |
Definition at line 250 of file 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.
Every instance of an invariant is ultimately generated by this function template, which is at times called via a wrapper function. Takes a backtrace, gives it to the reason structure, then aborts, printing reason.what() (which therefore includes the backtrace). In future this may throw reason
instead of aborting. Template parameter ET: type of exception to construct
file | : C string giving the name of the file. |
function | : C string giving the name of the function. |
line | : The line number of the invariant |
condition | : the condition this invariant is checking. |
params | : (variadic) parameters to forward to ET's constructor its backtrace member will be set before it is used. |
Definition at line 218 of file invariant.h.
void print_backtrace | ( | std::ostream & | out | ) |
Prints a back trace to 'out'.
out | Stream to print backtrace |
Definition at line 78 of file invariant.cpp.
void report_exception_to_stderr | ( | const invariant_failedt & | ) |
Dump exception report to stderr.
Definition at line 110 of file invariant.cpp.
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'.
Definition at line 354 of file invariant.h.