Loading...

Searching...

No Matches

Classes | Public Member Functions | Private Attributes | List of all members

scope_treet Class Reference

Tree to keep track of the destructors generated along each branch of a function. More...

#include <scope_tree.h>

+ Collaboration diagram for scope_treet:

[フレーム]

[legend]

Classes

struct declaration_statet

class scope_nodet

Public Member Functions

scope_treet ()

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.

std::optional< codet > & get_destructor (node_indext index)

Fetches the destructor value for the passed-in node index.

std::optional< declaration_statet > & get_declaration (node_indext index)

Fetches the declaration value for the passed-in node index.

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.

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.

void set_current_node (std::optional< node_indext > val)

Sets the current node.

void set_current_node (node_indext val)

Sets the current node.

node_indext get_current_node () const

Gets the node that the next addition will be added to as a child.

void descend_tree ()

Walks the current node down to its child.

void output_dot (std::ostream &os) const

Output scope tree to os in dot format.

Private Attributes

grapht< scope_nodet > scope_graph

node_indext current_node = 0

Detailed Description

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 92 of file scope_tree.h.

Constructor & Destructor Documentation

◆ scope_treet()

scope_treet::scope_treet ( )

inline

Definition at line 114 of file scope_tree.h.

Member Function Documentation

◆ add()

void scope_treet::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.

Parameters: destructor Code which is called when the current scope is left.

declaration Instruction which causes the scope to be entered.

Definition at line 11 of file scope_tree.cpp.

◆ descend_tree()

void scope_treet::descend_tree ( )

Walks the current node down to its child.

Definition at line 100 of file scope_tree.cpp.

◆ get_current_node()

node_indext scope_treet::get_current_node ( ) const

Gets the node that the next addition will be added to as a child.

Definition at line 109 of file scope_tree.cpp.

◆ get_declaration()

std::optional< scope_treet::declaration_statet > & scope_treet::get_declaration ( node_indext index )

Fetches the declaration value for the passed-in node index.

Definition at line 31 of file scope_tree.cpp.

◆ get_destructor()

std::optional< codet > & scope_treet::get_destructor ( node_indext index )

Fetches the destructor value for the passed-in node index.

Definition at line 24 of file scope_tree.cpp.

◆ get_destructors()

const std::vector< destructor_and_idt > scope_treet::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.

Parameters: 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.

Returns: collection of destructors that should be called for the range supplied.

Definition at line 68 of file scope_tree.cpp.

◆ get_nearest_common_ancestor_info()

const ancestry_resultt scope_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 37 of file scope_tree.cpp.

◆ output_dot()

void scope_treet::output_dot ( std::ostream & os ) const

inline

Output scope tree to os in dot format.

Definition at line 169 of file scope_tree.h.

◆ set_current_node() [1/2]

void scope_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 95 of file scope_tree.cpp.

◆ set_current_node() [2/2]

void scope_treet::set_current_node ( std::optional< 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 89 of file scope_tree.cpp.

Member Data Documentation

◆ current_node

node_indext scope_treet::current_node = 0

private

Definition at line 197 of file scope_tree.h.

◆ scope_graph

grapht<scope_nodet> scope_treet::scope_graph

private

Definition at line 196 of file scope_tree.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/scope_tree.h
/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/scope_tree.cpp