Loading...

Searching...

No Matches

invariant.cpp File Reference

#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'.

std::string get_backtrace ()

Returns a backtrace.

void report_exception_to_stderr (const invariant_failedt &reason)

Dump exception report to stderr.

Variables

bool cbmc_invariants_should_throw = false

Set this to true to cause invariants to throw a C++ exception rather than abort the program.

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.