cprover
|
#include "invariant.h"
#include "freer.h"
#include <memory>
#include <string>
#include <sstream>
#include <iostream>
#include <assert.h>
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... | |
std::string get_backtrace | ( | ) |
Returns a backtrace.
Definition at line 103 of file invariant.cpp.
void print_backtrace | ( | std::ostream & | out | ) |
Prints a back trace to 'out'.
out | Stream to print backtrace |
Definition at line 79 of file invariant.cpp.
void report_exception_to_stderr | ( | const invariant_failedt & | reason | ) |
Dump exception report to stderr.
Definition at line 111 of file invariant.cpp.
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 19 of file invariant.cpp.