#include "invariant.h"#include "freer.h"#include <memory>#include <sstream>#include <string>#include <iostream>#include <assert.h>
Include dependency graph for invariant.cpp:Go to the source code of this file.
Functions | |
| void | print_backtrace (std::ostream &out) |
| Prints a back trace to 'out'. More... | |
| std::string | get_backtrace () |
| Returns a backtrace. More... | |
| void | report_exception_to_stderr (const invariant_failedt &reason) |
| Dump exception report to stderr. More... | |
Variables | |
| bool | cbmc_invariants_should_throw = false |
| Set this to true to cause invariants to throw a C++ exception rather than abort the program. More... | |
Function Documentation
◆ get_backtrace()
| std::string get_backtrace | ( | ) |
Returns a backtrace.
- Returns
- backtrace with a file / function / line header.
Definition at line 141 of file invariant.cpp.
◆ print_backtrace()
| void print_backtrace | ( | std::ostream & | out | ) |
Prints a back trace to 'out'.
- Parameters
-
out Stream to print backtrace
Definition at line 88 of file invariant.cpp.
◆ report_exception_to_stderr()
| void report_exception_to_stderr | ( | const invariant_failedt & | reason | ) |
Dump exception report to stderr.
Definition at line 149 of file invariant.cpp.
Variable Documentation
◆ cbmc_invariants_should_throw
| bool cbmc_invariants_should_throw = false |
Set this to true to cause invariants to throw a C++ exception rather than abort the program.
This is currently untested behaviour, and may fail to clean up partly-completed CBMC operations or release resources. You should probably only use this to gather or report more information about the failure and then abort. Default off.
Definition at line 28 of file invariant.cpp.
