CBMC
|
A logic error, augmented with a distinguished field to hold a backtrace. More...
#include <c_errors.h>
Public Member Functions | |
virtual | ~invariant_failedt ()=default |
virtual std::string | what () const noexcept |
invariant_failedt (const std::string &_file, const std::string &_function, int _line, const std::string &_backtrace, const std::string &_condition, const std::string &_reason) | |
virtual | ~invariant_failedt ()=default |
virtual std::string | what () const noexcept |
invariant_failedt (const std::string &_file, const std::string &_function, int _line, const std::string &_backtrace, const std::string &_condition, const std::string &_reason) | |
Private Attributes | |
const std::string | file |
const std::string | function |
const int | line |
const std::string | backtrace |
const std::string | condition |
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, ...)
invariant_failedt is also the base class of any 'structured exceptions' - as found in file base_exceptions.h
Definition at line 27 of file c_errors.h.
|
virtualdefault |
|
inline |
Definition at line 42 of file c_errors.h.
|
virtualdefault |
|
inline |
Definition at line 124 of file invariant.h.
|
virtualnoexcept |
Reimplemented in invariant_with_diagnostics_failedt.
Definition at line 156 of file invariant.cpp.
|
virtualnoexcept |
Reimplemented in invariant_with_diagnostics_failedt.
|
private |
Definition at line 33 of file c_errors.h.
|
private |
Definition at line 34 of file c_errors.h.
|
private |
Definition at line 30 of file c_errors.h.
|
private |
Definition at line 31 of file c_errors.h.
|
private |
Definition at line 32 of file c_errors.h.
|
private |
Definition at line 35 of file c_errors.h.