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 
10 #include "invariant.h"
11 
12 #include <string>
13 #include <sstream>
14 
15 #include <iostream>
16 
17 // Backtraces compiler and C library specific
18 // So we should include something explicitly from the C library
19 // to check if the C library is glibc.
20 #include <assert.h>
21 #ifdef __GLIBC__
22 
23 // GCC needs LINKFLAGS="-rdynamic" to give function names in the backtrace
24 #include <execinfo.h>
25 #include <cxxabi.h>
26 
27 
37 static bool output_demangled_name(
38  std::ostream &out,
39  const std::string &stack_entry)
40 {
41  bool return_value=false;
42 
43  std::string working(stack_entry);
44 
45  std::string::size_type start=working.rfind('('); // Path may contain '(' !
46  std::string::size_type end=working.find('+', start);
47 
48  if(start!=std::string::npos &&
49  end!=std::string::npos &&
50  start+1<=end-1)
51  {
52  std::string::size_type length=end-(start+1);
53  std::string mangled(working.substr(start+1, length));
54 
55  int demangle_success=1;
56  char *demangled=
57  abi::__cxa_demangle(mangled.c_str(), nullptr, nullptr, &demangle_success);
58 
59  if(demangle_success==0)
60  {
61  out << working.substr(0, start+1)
62  << demangled
63  << working.substr(end);
64  return_value=true;
65  }
66 
67  free(demangled);
68  }
69 
70  return return_value;
71 }
72 #endif
73 
74 
78  std::ostream &out)
79 {
80 #ifdef __GLIBC__
81  out << "Backtrace\n" << std::flush;
82 
83  void * stack[50] = {};
84 
85  std::size_t entries=backtrace(stack, sizeof(stack) / sizeof(void *));
86  char **description=backtrace_symbols(stack, entries);
87 
88  for(std::size_t i=0; i<entries; i++)
89  {
90  if(!output_demangled_name(out, description[i]))
91  out << description[i];
92  out << '\n' << std::flush;
93  }
94 
95  free(description);
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  << "Backtrace:\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:77
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
unsignedbv_typet size_type()
Definition: c_types.cpp:57
void free(void *)
std::string get_backtrace()
Returns a backtrace.
Definition: invariant.cpp:104
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