37 static bool output_demangled_name(
39 const std::string &stack_entry)
41 bool return_value=
false;
43 std::string working(stack_entry);
48 if(start!=std::string::npos &&
49 end!=std::string::npos &&
53 std::string mangled(working.substr(start+1, length));
55 int demangle_success=1;
57 abi::__cxa_demangle(mangled.c_str(),
nullptr,
nullptr, &demangle_success);
59 if(demangle_success==0)
61 out << working.substr(0, start+1)
63 << working.substr(end);
81 out <<
"Backtrace\n" << std::flush;
83 void *
stack[50] = {};
85 std::size_t entries=backtrace(
stack,
sizeof(
stack) /
sizeof(
void *));
86 char **description=backtrace_symbols(
stack, entries);
88 for(std::size_t i=0; i<entries; i++)
90 if(!output_demangled_name(out, description[i]))
91 out << description[i];
92 out <<
'\n' << std::flush;
98 out <<
"Backtraces not supported\n" << std::flush;
106 std::ostringstream ostr;
114 std::cerr <<
"--- begin invariant violation report ---\n";
115 std::cerr << reason.what() <<
'\n';
116 std::cerr <<
"--- end invariant violation report ---\n";
120 const std::string &
file,
121 const std::string &
function,
123 const std::string &backtrace,
124 const std::string &reason)
126 std::ostringstream out;
127 out <<
"Invariant check failed\n" 129 <<
" function " <<
function 130 <<
" line " <<
line <<
'\n' A logic error, augmented with a distinguished field to hold a backtrace.
void print_backtrace(std::ostream &out)
Prints a back trace to 'out'.
std::string get_invariant_failed_message(const std::string &file, const std::string &function, int line, const std::string &backtrace, const std::string &reason)
unsignedbv_typet size_type()
std::string get_backtrace()
Returns a backtrace.
const std::string backtrace
void report_exception_to_stderr(const invariant_failedt &reason)
Dump exception report to stderr.
const irept & find(const irep_namet &name) const