cprover
destructor_tree.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Destructor Tree
4 
5  Author: John Dumbell, john.dumbell@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
10 #define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
11 
12 #include <util/graph.h>
13 #include <util/std_code.h>
14 
15 typedef std::size_t node_indext;
16 
21 {
22 public:
24  : common_ancestor(node),
27  {
28  }
30  node_indext node,
31  std::size_t left_pre_size,
32  std::size_t right_pre_size)
33  : common_ancestor(node),
34  left_depth_below_common_ancestor(left_pre_size),
35  right_depth_below_common_ancestor(right_pre_size)
36  {
37  }
41 };
42 
46 {
47 public:
49  : destructor(code), node_id(id)
50  {
51  }
52 
55 };
56 
89 {
90 public:
92  {
93  // We add a default node to the graph to act as a root for path traversal.
94  this->destruction_graph.add_node();
95  }
96 
99  void add(const codet &destructor);
100 
103 
112  const std::vector<destructor_and_idt> get_destructors(
113  optionalt<node_indext> end_index = {},
114  optionalt<node_indext> starting_index = {});
115 
120  node_indext left_index,
121  node_indext right_index);
122 
127 
130  void set_current_node(node_indext val);
131 
134 
136  void descend_tree();
137 
138 private:
139  class destructor_nodet : public graph_nodet<empty_edget>
140  {
141  public:
142  destructor_nodet() = default;
143 
144  explicit destructor_nodet(codet destructor)
145  : destructor_value(std::move(destructor))
146  {
147  }
149  };
150 
153 };
154 
155 #endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
Result of an attempt to find ancestor information about two nodes.
std::size_t left_depth_below_common_ancestor
ancestry_resultt(node_indext node)
std::size_t right_depth_below_common_ancestor
node_indext common_ancestor
ancestry_resultt(node_indext node, std::size_t left_pre_size, std::size_t right_pre_size)
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
Result of a tree query holding both destructor codet and the ID of the node that held it.
const codet destructor
destructor_and_idt(const codet &code, node_indext id)
Tree to keep track of the destructors generated along each branch of a function.
void set_current_node(optionalt< node_indext > val)
Sets the current node.
void add(const codet &destructor)
Adds a destructor to the current stack, attaching itself to the current node.
const std::vector< destructor_and_idt > get_destructors(optionalt< node_indext > end_index={}, optionalt< node_indext > starting_index={})
Builds a vector of destructors that start from starting_index and ends at end_index.
grapht< destructor_nodet > destruction_graph
void descend_tree()
Walks the current node down to its child.
node_indext current_node
const ancestry_resultt get_nearest_common_ancestor_info(node_indext left_index, node_indext right_index)
Finds the nearest common ancestor of two nodes and then returns it.
optionalt< codet > & get_destructor(node_indext index)
Fetches the destructor value for the passed-in node index.
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
This class represents a node in a directed graph.
Definition: graph.h:35
A generic directed graph with a parametric node type.
Definition: graph.h:167
std::size_t node_indext
A Template Class for Graphs.
nonstd::optional< T > optionalt
Definition: optional.h:35