cprover
Loading...
Searching...
No Matches
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
15typedef std::size_t node_indext;
16
21{
22public:
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),
36 {
37 }
41};
42
46{
47public:
49 : destructor(code), node_id(id)
50 {
51 }
52
55};
56
89{
90public:
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
131
134
136 void descend_tree();
137
138private:
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_base.h:29
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.
STL namespace.
nonstd::optional< T > optionalt
Definition: optional.h:35