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

A class that includes diagnostic information related to an invariant violation. More...

#include <invariant.h>

+ Inheritance diagram for invariant_with_diagnostics_failedt:
+ Collaboration diagram for invariant_with_diagnostics_failedt:

Public Member Functions

virtual std::string what () const noexcept
 
 invariant_with_diagnostics_failedt (const std::string &_file, const std::string &_function, int _line, const std::string &_backtrace, const std::string &_condition, const std::string &_reason, const std::string &_diagnostics)
 
- Public Member Functions inherited from invariant_failedt
virtual ~invariant_failedt ()=default
 
 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
 
 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 diagnostics
 

Detailed Description

A class that includes diagnostic information related to an invariant violation.

Definition at line 143 of file invariant.h.

Constructor & Destructor Documentation

◆ invariant_with_diagnostics_failedt()

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

Definition at line 151 of file invariant.h.

Member Function Documentation

◆ what()

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

Reimplemented from invariant_failedt.

Definition at line 168 of file invariant.cpp.

Member Data Documentation

◆ diagnostics

const std::string invariant_with_diagnostics_failedt::diagnostics
private

Definition at line 146 of file invariant.h.

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