cprover
invariant_failedt Class Reference

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

#include <invariant.h>

Inheritance diagram for invariant_failedt:
[legend]
Collaboration diagram for invariant_failedt:
[legend]

Public Member Functions

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, ...)

Definition at line 75 of file invariant.h.

Constructor & Destructor Documentation

◆ invariant_failedt()

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 88 of file invariant.h.

Member Function Documentation

◆ what()

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

Definition at line 117 of file invariant.cpp.

References backtrace, condition, line, and reason.

Referenced by report_exception_to_stderr().

Member Data Documentation

◆ backtrace

const std::string invariant_failedt::backtrace
private

Definition at line 81 of file invariant.h.

Referenced by what().

◆ condition

const std::string invariant_failedt::condition
private

Definition at line 82 of file invariant.h.

Referenced by what().

◆ file

const std::string invariant_failedt::file
private

Definition at line 78 of file invariant.h.

◆ function

const std::string invariant_failedt::function
private

Definition at line 79 of file invariant.h.

◆ line

const int invariant_failedt::line
private

Definition at line 80 of file invariant.h.

Referenced by what().

◆ reason

const std::string invariant_failedt::reason
private

Definition at line 83 of file invariant.h.

Referenced by what().


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