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 "util/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 #ifdef __GLIBC__
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 #ifdef __GLIBC__
82  out << "Backtrace\n" << std::flush;
83 
84  void * stack[50] = {};
85 
86  std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *));
87  std::unique_ptr<char*, freert> description(
88  backtrace_symbols(stack, entries));
89 
90  for(std::size_t i=0; i<entries; i++)
91  {
92  if(!output_demangled_name(out, description.get()[i]))
93  out << description.get()[i];
94  out << '\n' << std::flush;
95  }
96 
97 #else
98  out << "Backtraces not supported\n" << std::flush;
99 #endif
100 }
101 
104 std::string get_backtrace()
105 {
106  std::ostringstream ostr;
107  print_backtrace(ostr);
108  return ostr.str();
109 }
110 
113 {
114  std::cerr << "--- begin invariant violation report ---\n";
115  std::cerr << reason.what() << '\n';
116  std::cerr << "--- end invariant violation report ---\n";
117 }
118 
120  const std::string &file,
121  const std::string &function,
122  int line,
123  const std::string &backtrace,
124  const std::string &reason)
125 {
126  std::ostringstream out;
127  out << "Invariant check failed\n"
128  << "File " << file
129  << " function " << function
130  << " line " << line << '\n'
131  << "Reason: " << reason
132  << "\nBacktrace:\n"
133  << backtrace << '\n';
134  return out.str();
135 }
A logic error, augmented with a distinguished field to hold a backtrace.
Definition: invariant.h:75
void print_backtrace(std::ostream &out)
Prints a back trace to &#39;out&#39;.
Definition: invariant.cpp:78
std::string get_invariant_failed_message(const std::string &file, const std::string &function, int line, const std::string &backtrace, const std::string &reason)
Definition: invariant.cpp:119
const int line
Definition: invariant.h:88
unsignedbv_typet size_type()
Definition: c_types.cpp:58
const std::string reason
Definition: invariant.h:90
std::string get_backtrace()
Returns a backtrace.
Definition: invariant.cpp:104
const std::string backtrace
Definition: invariant.h:89
void report_exception_to_stderr(const invariant_failedt &reason)
Dump exception report to stderr.
Definition: invariant.cpp:112
#define stack(x)
Definition: parser.h:144
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
Definition: kdev_t.h:19