9 #ifndef CPROVER_UTIL_INVARIANT_H 10 #define CPROVER_UTIL_INVARIANT_H 13 #include <type_traits> 79 const std::string &
file,
80 const std::string &
function,
83 const std::string &
reason);
88 const std::string
function;
94 const std::string &_file,
95 const std::string &_function,
97 const std::string &_backtrace,
98 const std::string &_reason):
115 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT) 117 #define INVARIANT(CONDITION, REASON) \ 118 __CPROVER_assert((CONDITION), "Invariant : " REASON) 121 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK) 126 #define INVARIANT(CONDITION, REASON, ...) do {} while(0) 128 #elif defined(CPROVER_INVARIANT_ASSERT) 132 #define INVARIANT(CONDITION, REASON, ...) assert((CONDITION) && ((REASON), true)) 151 template<
class ET,
typename ...Params>
155 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
157 const std::string &
file,
158 const std::string &
function,
163 ET to_throw(
file,
function, line, backtrace, std::forward<Params>(params)...);
181 const std::string &
file,
182 const std::string &
function,
184 const std::string &reason)
186 invariant_violated_structured<invariant_failedt>(
197 #define __this_function__ __FUNCTION__ 199 #define __this_function__ __func__ 202 #define INVARIANT(CONDITION, REASON) \ 206 invariant_violated_string(__FILE__, __this_function__, __LINE__, (REASON)); \ 209 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ 213 invariant_violated_structured<TYPENAME>(__FILE__, __this_function__, __LINE__, __VA_ARGS__); \ 216 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block 225 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition") 226 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ 227 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 232 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition") 233 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ 234 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 240 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value") 241 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \ 242 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 245 #define UNREACHABLE INVARIANT(false, "Unreachable") 246 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ 247 INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__) 252 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON) 253 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ 254 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 260 #define TODO INVARIANT(0, "Todo") 261 #define UNIMPLEMENTED INVARIANT(0, "Unimplemented") 262 #define UNHANDLED_CASE INVARIANT(0, "Unhandled case") 264 #endif // CPROVER_UTIL_INVARIANT_H A logic error, augmented with a distinguished field to hold a backtrace.
std::string get_invariant_failed_message(const std::string &file, const std::string &function, int line, const std::string &backtrace, const std::string &reason)
void print_backtrace(std::ostream &out)
Prints a back trace to 'out'.
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.
void invariant_violated_string(const std::string &file, const std::string &function, const int line, const std::string &reason)
Takes a backtrace, constructs an invariant_violatedt from reason and the backtrace, aborts printing the invariant's description.
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, Params &&... params)
Takes a backtrace, gives it to the reason structure, then aborts, printing reason.what() (which therefore includes the backtrace).
invariant_failedt(const std::string &_file, const std::string &_function, int _line, const std::string &_backtrace, const std::string &_reason)