CBMC
invariant_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Invariant helper utilities
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "invariant_utils.h"
13 
14 #include "irep.h"
15 
17  const irept &problem_node,
18  const std::string &description)
19 {
20  if(problem_node.is_nil())
21  return description;
22  else
23  {
24  std::string ret=description;
25  ret+="\nProblem irep:\n";
26  ret+=problem_node.pretty(0,0);
27  return ret;
28  }
29 }
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
bool is_nil() const
Definition: irep.h:364
std::string pretty_print_invariant_with_irep(const irept &problem_node, const std::string &description)
Produces a plain string error description from an irep and some explanatory text.