cprover
Loading...
Searching...
No Matches
destructor_tree.cpp
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#include "destructor_tree.h"
10
11void destructor_treet::add(const codet &destructor)
12{
14 auto new_node = destruction_graph.add_node(destructor);
17}
18
20{
21 PRECONDITION(index < destruction_graph.size());
22 return destruction_graph[index].destructor_value;
23}
24
28{
29 std::size_t left_unique_count = 0, right_unique_count = 0;
30 while(right_index != left_index)
31 {
33 {
36 !edge_map.empty(),
37 "Node at index " + std::to_string(right_index) +
38 " has no parent, can't find an ancestor.");
39 right_index = edge_map.begin()->first, right_unique_count++;
40 }
41 else
42 {
45 !edge_map.empty(),
46 "Node at index " + std::to_string(left_index) +
47 " has no parent, can't find an ancestor.");
48 left_index = edge_map.begin()->first, left_unique_count++;
49 }
50 }
51
52 // At this point it dosen't matter which index we return as both are the same.
54}
55
56const std::vector<destructor_and_idt> destructor_treet::get_destructors(
59{
60 node_indext next_id = starting_index.value_or(get_current_node());
61 node_indext end_id = end_index.value_or(0);
62
63 std::vector<destructor_and_idt> codes;
64 while(next_id > end_id)
65 {
66 auto node = destruction_graph[next_id];
67 auto &destructor = node.destructor_value;
68 if(destructor)
69 codes.emplace_back(destructor_and_idt(*destructor, next_id));
70
71 next_id = node.in.begin()->first;
72 }
73
74 return codes;
75}
76
82
87
96
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Result of an attempt to find ancestor information about two nodes.
Data structure for representing an arbitrary statement in a program.
Result of a tree query holding both destructor codet and the ID of the node that held it.
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.
std::size_t node_indext
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423