CBMC
Public Member Functions | Private Attributes | List of all members
invariant_failedt Class Reference

A logic error, augmented with a distinguished field to hold a backtrace. More...

#include <c_errors.h>

+ Inheritance diagram for invariant_failedt:
+ Collaboration diagram for invariant_failedt:

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
 

Detailed Description

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.

Constructor & Destructor Documentation

◆ ~invariant_failedt() [1/2]

virtual invariant_failedt::~invariant_failedt ( )
virtualdefault

◆ invariant_failedt() [1/2]

invariant_failedt::invariant_failedt ( const std::string &  _file,
const std::string &  _function,
int  _line,
const std::string &  _backtrace,
const std::string &  _condition,
const std::string &  _reason 
)
inline

Definition at line 42 of file c_errors.h.

◆ ~invariant_failedt() [2/2]

virtual invariant_failedt::~invariant_failedt ( )
virtualdefault

◆ invariant_failedt() [2/2]

invariant_failedt::invariant_failedt ( const std::string &  _file,
const std::string &  _function,
int  _line,
const std::string &  _backtrace,
const std::string &  _condition,
const std::string &  _reason 
)
inline

Definition at line 124 of file invariant.h.

Member Function Documentation

◆ what() [1/2]

std::string invariant_failedt::what ( ) const
virtualnoexcept

Reimplemented in invariant_with_diagnostics_failedt.

Definition at line 156 of file invariant.cpp.

◆ what() [2/2]

virtual std::string invariant_failedt::what ( ) const
virtualnoexcept

Reimplemented in invariant_with_diagnostics_failedt.

Member Data Documentation

◆ backtrace

const std::string invariant_failedt::backtrace
private

Definition at line 33 of file c_errors.h.

◆ condition

const std::string invariant_failedt::condition
private

Definition at line 34 of file c_errors.h.

◆ file

const std::string invariant_failedt::file
private

Definition at line 30 of file c_errors.h.

◆ function

const std::string invariant_failedt::function
private

Definition at line 31 of file c_errors.h.

◆ line

const int invariant_failedt::line
private

Definition at line 32 of file c_errors.h.

◆ reason

const std::string invariant_failedt::reason
private

Definition at line 35 of file c_errors.h.

The documentation for this class was generated from the following files: