cprover
invariant.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Martin Brain, martin.brain@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include "invariant.h"
10 
11 #include "freer.h"
12 
13 #include <memory>
14 #include <string>
15 #include <sstream>
16 
17 #include <iostream>
18 
20 
21 // Backtraces compiler and C library specific
22 // So we should include something explicitly from the C library
23 // to check if the C library is glibc.
24 #include <assert.h>
25 #if defined(__GLIBC__) || defined(__APPLE__)
26 
27 // GCC needs LINKFLAGS="-rdynamic" to give function names in the backtrace
28 #include <execinfo.h>
29 #include <cxxabi.h>
30 
40 static bool output_demangled_name(
41  std::ostream &out,
42  const std::string &stack_entry)
43 {
44  bool return_value=false;
45 
46  std::string working(stack_entry);
47 
48  std::string::size_type start=working.rfind('('); // Path may contain '(' !
49  std::string::size_type end=working.find('+', start);
50 
51  if(start!=std::string::npos &&
52  end!=std::string::npos &&
53  start+1<=end-1)
54  {
55  std::string::size_type length=end-(start+1);
56  std::string mangled(working.substr(start+1, length));
57 
58  int demangle_success=1;
59  std::unique_ptr<char, freert> demangled(
60  abi::__cxa_demangle(
61  mangled.c_str(), nullptr, nullptr, &demangle_success));
62 
63  if(demangle_success==0)
64  {
65  out << working.substr(0, start+1)
66  << demangled.get()
67  << working.substr(end);
68  return_value=true;
69  }
70  }
71 
72  return return_value;
73 }
74 #endif
75 
76 
80  std::ostream &out)
81 {
82 #if defined(__GLIBC__) || defined(__APPLE__)
83  void * stack[50] = {};
84 
85  std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *));
86  std::unique_ptr<char*, freert> description(
87  backtrace_symbols(stack, entries));
88 
89  for(std::size_t i=0; i<entries; i++)
90  {
91  if(!output_demangled_name(out, description.get()[i]))
92  out << description.get()[i];
93  out << '\n' << std::flush;
94  }
95 
96 #else
97  out << "Backtraces not supported\n" << std::flush;
98 #endif
99 }
100 
103 std::string get_backtrace()
104 {
105  std::ostringstream ostr;
106  print_backtrace(ostr);
107  return ostr.str();
108 }
109 
112 {
113  std::cerr << "--- begin invariant violation report ---\n";
114  std::cerr << reason.what() << '\n';
115  std::cerr << "--- end invariant violation report ---\n";
116 }
117 
118 std::string invariant_failedt::what() const noexcept
119 {
120  std::ostringstream out;
121  out << "Invariant check failed\n"
122  << "File: " << file << ":" << line << " function: " << function << '\n'
123  << "Condition: " << condition << '\n'
124  << "Reason: " << reason << '\n'
125  << "Backtrace:" << '\n'
126  << backtrace << '\n';
127  return out.str();
128 }
129 
130 std::string invariant_with_diagnostics_failedt::what() const noexcept
131 {
132  std::string s(invariant_failedt::what());
133 
134  if(!s.empty() && s.back() != '\n')
135  s += '\n';
136 
137  return s + "Diagnostics: " + diagnostics + '\n';
138 }
invariant_failedt::condition
const std::string condition
Definition: invariant.h:117
print_backtrace
void print_backtrace(std::ostream &out)
Prints a back trace to 'out'.
Definition: invariant.cpp:79
invariant_failedt
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: invariant.h:111
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
file
Definition: kdev_t.h:19
invariant_with_diagnostics_failedt::diagnostics
const std::string diagnostics
Definition: invariant.h:147
report_exception_to_stderr
void report_exception_to_stderr(const invariant_failedt &reason)
Dump exception report to stderr.
Definition: invariant.cpp:111
invariant_failedt::line
const int line
Definition: invariant.h:115
invariant_failedt::reason
const std::string reason
Definition: invariant.h:118
invariant_failedt::backtrace
const std::string backtrace
Definition: invariant.h:116
freer.h
get_backtrace
std::string get_backtrace()
Returns a backtrace.
Definition: invariant.cpp:103
invariant.h
invariant_failedt::what
virtual std::string what() const noexcept
Definition: invariant.cpp:118
invariant_with_diagnostics_failedt::what
virtual std::string what() const noexcept
Definition: invariant.cpp:130
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
cbmc_invariants_should_throw
bool cbmc_invariants_should_throw
Set this to true to cause invariants to throw a C++ exception rather than abort the program.
Definition: invariant.cpp:19