12 const codet &destructor,
13 std::optional<goto_programt::targett> declaration)
30std::optional<scope_treet::declaration_statet> &
50 " has no parent, can't find an ancestor.");
58 "Node at index " + std::to_string(
left_index) +
59 " has no parent, can't find an ancestor.");
75 std::vector<destructor_and_idt>
codes;
79 auto &destructor = node.destructor_value;
83 next_id = node.in.begin()->first;
116 std::optional<declaration_statet> declaration)
117 : destructor_value(
std::move(destructor)), declaration(
std::move(declaration))
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.
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.
grapht< scope_nodet > scope_graph
std::optional< declaration_statet > & get_declaration(node_indext index)
Fetches the declaration value for the passed-in node index.
void add(const codet &destructor, std::optional< goto_programt::targett > declaration)
Adds a destructor/declaration pair to the current stack, attaching it to the current node.
void descend_tree()
Walks the current node down to its child.
void set_current_node(std::optional< node_indext > val)
Sets the current node.
const std::vector< destructor_and_idt > get_destructors(std::optional< node_indext > end_index={}, std::optional< node_indext > starting_index={})
Builds a vector of destructors that start from starting_index and ends at end_index.
std::optional< 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.
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.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.