CBMC
|
Tree to keep track of the destructors generated along each branch of a function. More...
#include <destructor_tree.h>
Classes | |
class | destructor_nodet |
Public Member Functions | |
destructor_treet () | |
void | add (const codet &destructor) |
Adds a destructor to the current stack, attaching itself to the current node. More... | |
optionalt< codet > & | get_destructor (node_indext index) |
Fetches the destructor value for the passed-in node index. More... | |
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. More... | |
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. More... | |
void | set_current_node (optionalt< node_indext > val) |
Sets the current node. More... | |
void | set_current_node (node_indext val) |
Sets the current node. More... | |
node_indext | get_current_node () const |
Gets the node that the next addition will be added to as a child. More... | |
void | descend_tree () |
Walks the current node down to its child. More... | |
Private Attributes | |
grapht< destructor_nodet > | destruction_graph |
node_indext | current_node = 0 |
Tree to keep track of the destructors generated along each branch of a function.
Used to compare and find out what dead instructions are needed when moving from one branch to another.
For example, if you had this code:
object a; if (enabled) object b; object c; else object e;
It would generate a tree like this:
-> b -> c
Root -> a -> e
Where each split represents a different block and each letter represents the destructor codet for that particular variable.
To find out anything interesting you need to get a node ID (currently only got by calling get_current_node at a particular point in the tree) and then use that later to compare against a different point in the tree.
So if I took note of the nodes at the end of each branch (c, e) and wanted to compare them, I'd find that 'a' is the common ancestor, and the steps required to get there from 'c' was 2 and 'e' was 1, which also tells you if a certain branch is a prefix or not. In this case neither are a prefix of the other.
Definition at line 88 of file destructor_tree.h.
|
inline |
Definition at line 91 of file destructor_tree.h.
void destructor_treet::add | ( | const codet & | destructor | ) |
Adds a destructor to the current stack, attaching itself to the current node.
Definition at line 11 of file destructor_tree.cpp.
void destructor_treet::descend_tree | ( | ) |
Walks the current node down to its child.
Definition at line 88 of file destructor_tree.cpp.
node_indext destructor_treet::get_current_node | ( | ) | const |
Gets the node that the next addition will be added to as a child.
Definition at line 97 of file destructor_tree.cpp.
optionalt< codet > & destructor_treet::get_destructor | ( | node_indext | index | ) |
Fetches the destructor value for the passed-in node index.
Definition at line 19 of file destructor_tree.cpp.
const std::vector< destructor_and_idt > destructor_treet::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.
end_index | Index of the first variable to keep. List won't include this node. If empty, root of the current stack. |
starting_index | Index of the first variable to destroy. If empty, top of the current stack. |
Definition at line 56 of file destructor_tree.cpp.
const ancestry_resultt destructor_treet::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.
This should be used when you want to find out what parts of the two branches are common to each other.
Definition at line 25 of file destructor_tree.cpp.
void destructor_treet::set_current_node | ( | node_indext | val | ) |
Sets the current node.
Next time a node is added to the stack it will be added as a child of this node.
Definition at line 83 of file destructor_tree.cpp.
void destructor_treet::set_current_node | ( | optionalt< node_indext > | val | ) |
Sets the current node.
Next time a node is added to the stack it will be added as a child of this node. If passed an empty index, no assignment will be done.
Definition at line 77 of file destructor_tree.cpp.
|
private |
Definition at line 152 of file destructor_tree.h.
|
private |
Definition at line 151 of file destructor_tree.h.