9 #ifndef CPROVER_UTIL_INVARIANT_H 10 #define CPROVER_UTIL_INVARIANT_H 13 #include <type_traits> 79 const std::string
function;
86 std::string
what() const noexcept;
89 const
std::
string &_file,
90 const
std::
string &_function,
92 const
std::
string &_backtrace,
93 const
std::
string &_condition,
94 const
std::
string &_reason)
105 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT) 107 #define INVARIANT(CONDITION, REASON) \ 108 __CPROVER_assert((CONDITION), "Invariant : " REASON) 110 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ 111 INVARIANT(CONDITION, "") 113 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK) 118 #define INVARIANT(CONDITION, REASON) do {} while(false) 119 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false) 121 #elif defined(CPROVER_INVARIANT_ASSERT) 125 #define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true)) 127 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION)) 146 template <
class ET,
typename... Params>
150 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
152 const std::string &
file,
153 const std::string &
function,
155 const std::string &condition,
165 std::forward<Params>(params)...);
185 const std::string &
file,
186 const std::string &
function,
188 const std::string &reason,
189 const std::string &condition)
191 invariant_violated_structured<invariant_failedt>(
192 file,
function, line, condition, reason);
199 #define __this_function__ __FUNCTION__ 201 #define __this_function__ __func__ 204 #define INVARIANT(CONDITION, REASON) \ 208 invariant_violated_string( \ 216 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ 220 invariant_violated_structured<TYPENAME>( \ 228 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block 242 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition") 243 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ 244 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 254 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition") 255 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ 256 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 266 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value") 267 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \ 268 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 271 #define UNREACHABLE INVARIANT(false, "Unreachable") 272 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ 273 INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__) 278 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON) 279 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ 280 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 286 #define TODO INVARIANT(false, "Todo") 287 #define UNIMPLEMENTED INVARIANT(false, "Unimplemented") 288 #define UNHANDLED_CASE INVARIANT(false, "Unhandled case") 290 #endif // CPROVER_UTIL_INVARIANT_H std::string what() const noexcept
A logic error, augmented with a distinguished field to hold a backtrace.
const std::string condition
void print_backtrace(std::ostream &out)
Prints a back trace to 'out'.
void invariant_violated_string(const std::string &file, const std::string &function, const int line, const std::string &reason, const std::string &condition)
Takes a backtrace, constructs an invariant_violatedt from reason and the backtrace, aborts printing the invariant's description.
const std::string function
const std::string backtrace
std::string get_backtrace()
Returns a backtrace.
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)
Takes a backtrace, gives it to the reason structure, then aborts, printing reason.what() (which therefore includes the backtrace).