cprover
|
A logic error, augmented with a distinguished field to hold a backtrace. More...
#include <invariant.h>
Public Member Functions | |
invariant_failedt (const std::string &_file, const std::string &_function, int _line, const std::string &_backtrace, const std::string &_reason) | |
Public Attributes | |
const std::string | file |
const std::string | function |
const int | line |
const std::string | backtrace |
const std::string | reason |
Private Member Functions | |
std::string | get_invariant_failed_message (const std::string &file, const std::string &function, int line, const std::string &backtrace, const std::string &reason) |
A logic error, augmented with a distinguished field to hold a backtrace.
Classes that extend this one should share the same initial constructor parameters: their constructor signature should be of the form: my_invariantt::my_invariantt( const std::string &file, const std::string &function, int line, const std::string &backtrace, T1 arg1, T2 arg2 ... Tn argn) It should pretty-print the T1 ... Tn arguments and pass it as reason
to invariant_failedt's constructor, or else simply pass a reason string through. Conforming to this pattern allows the class to be used with the INVARIANT family of macros, allowing constructs like INVARIANT(x==y, my_invariantt, (T1)actual1, (T2)actual2, ...)
Definition at line 75 of file invariant.h.
|
inline |
Definition at line 93 of file invariant.h.
|
private |
Definition at line 119 of file invariant.cpp.
const std::string invariant_failedt::backtrace |
Definition at line 90 of file invariant.h.
Referenced by get_invariant_failed_message().
const std::string invariant_failedt::file |
Definition at line 87 of file invariant.h.
const std::string invariant_failedt::function |
Definition at line 88 of file invariant.h.
const int invariant_failedt::line |
Definition at line 89 of file invariant.h.
Referenced by get_invariant_failed_message().
const std::string invariant_failedt::reason |
Definition at line 91 of file invariant.h.
Referenced by get_invariant_failed_message().