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);
87 const std::string
function;
93 const std::string &_file,
94 const std::string &_function,
96 const std::string &_backtrace,
97 const std::string &_reason):
114 #if defined(CPROVER_INVARIANT_CPROVER_ASSERT) 116 #define INVARIANT(CONDITION, REASON) \ 117 __CPROVER_assert((CONDITION), "Invariant : " REASON) 119 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ 120 INVARIANT(CONDITION, "") 122 #elif defined(CPROVER_INVARIANT_DO_NOT_CHECK) 127 #define INVARIANT(CONDITION, REASON) do {} while(false) 128 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) do {} while(false) 130 #elif defined(CPROVER_INVARIANT_ASSERT) 134 #define INVARIANT(CONDITION, REASON) assert((CONDITION) && ((REASON), true)) 136 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) assert((CONDITION)) 154 template<
class ET,
typename ...Params>
158 typename std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type
160 const std::string &
file,
161 const std::string &
function,
166 ET to_throw(
file,
function, line, backtrace, std::forward<Params>(params)...);
184 const std::string &
file,
185 const std::string &
function,
187 const std::string &reason)
189 invariant_violated_structured<invariant_failedt>(
200 #define __this_function__ __FUNCTION__ 202 #define __this_function__ __func__ 205 #define INVARIANT(CONDITION, REASON) \ 209 invariant_violated_string( \ 210 __FILE__, __this_function__, __LINE__, (REASON)); \ 213 #define INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ 217 invariant_violated_structured<TYPENAME>( \ 218 __FILE__, __this_function__, __LINE__, __VA_ARGS__); \ 221 #endif // End CPROVER_DO_NOT_CHECK / CPROVER_ASSERT / ... if block 230 #define PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition") 231 #define PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ 232 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 237 #define POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition") 238 #define POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) \ 239 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 245 #define CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value") 246 #define CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) \ 247 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 250 #define UNREACHABLE INVARIANT(false, "Unreachable") 251 #define UNREACHABLE_STRUCTURED(TYPENAME, ...) \ 252 INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__) 257 #define DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON) 258 #define DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) \ 259 INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__) 265 #define TODO INVARIANT(false, "Todo") 266 #define UNIMPLEMENTED INVARIANT(false, "Unimplemented") 267 #define UNHANDLED_CASE INVARIANT(false, "Unhandled case") 269 #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)