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