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

 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)
 

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 &  _reason 
)
inline

Definition at line 93 of file invariant.h.

Member Function Documentation

◆ get_invariant_failed_message()

std::string invariant_failedt::get_invariant_failed_message ( const std::string &  file,
const std::string &  function,
int  line,
const std::string &  backtrace,
const std::string &  reason 
)
private

Definition at line 119 of file invariant.cpp.

References backtrace, line, and reason.

Member Data Documentation

◆ backtrace

const std::string invariant_failedt::backtrace

Definition at line 90 of file invariant.h.

Referenced by get_invariant_failed_message().

◆ file

const std::string invariant_failedt::file

Definition at line 87 of file invariant.h.

◆ function

const std::string invariant_failedt::function

Definition at line 88 of file invariant.h.

◆ line

const int invariant_failedt::line

Definition at line 89 of file invariant.h.

Referenced by get_invariant_failed_message().

◆ reason

const std::string invariant_failedt::reason

Definition at line 91 of file invariant.h.

Referenced by get_invariant_failed_message().


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