9#ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
10#define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
Result of a tree query holding both destructor codet and the ID of the node that held it.
destructor_and_idt(const codet &code, node_indext id)
optionalt< codet > destructor_value
destructor_nodet(codet destructor)
destructor_nodet()=default
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.
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.
A Template Class for Graphs.