destructor_tree.h

Go to the documentation of this file.

/*******************************************************************\
 
 Module: Destructor Tree
 
 Author: John Dumbell, john.dumbell@diffblue.com
 
\*******************************************************************/
 
#ifndef CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
#define CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H
 
#include <util/graph.h>
#include <util/std_code.h>
 
typedef std::size_t node_indext;
 
class ancestry_resultt
{
public:
  explicit ancestry_resultt(node_indext node)
    : common_ancestor(node),
      left_depth_below_common_ancestor(0),
      right_depth_below_common_ancestor(0)
  {
  }
  ancestry_resultt(
    node_indext node,
    std::size_t left_pre_size,
    std::size_t right_pre_size)
    : common_ancestor(node),
      left_depth_below_common_ancestor(left_pre_size),
      right_depth_below_common_ancestor(right_pre_size)
  {
  }
  node_indext common_ancestor;
  std::size_t left_depth_below_common_ancestor;
  std::size_t right_depth_below_common_ancestor;
};
 
class destructor_and_idt
{
public:
  destructor_and_idt(const codet &code, node_indext id)
    : destructor(code), node_id(id)
  {
  }
 
  const codet destructor;
  node_indext node_id;
};
 
class destructor_treet
{
public:
  destructor_treet()
  {
    // We add a default node to the graph to act as a root for path traversal.
    this->destruction_graph.add_node();
  }
 
  void add(const codet &destructor);
 
  optionalt<codet> &get_destructor(node_indext index);
 
  const std::vector<destructor_and_idt> get_destructors(
    optionalt<node_indext> end_index = {},
    optionalt<node_indext> starting_index = {});
 
  const ancestry_resultt get_nearest_common_ancestor_info(
    node_indext left_index,
    node_indext right_index);
 
  void set_current_node(optionalt<node_indext> val);
 
  void set_current_node(node_indext val);
 
  node_indext get_current_node() const;
 
  void descend_tree();
 
private:
  class destructor_nodet : public graph_nodet<empty_edget>
  {
  public:
    destructor_nodet() = default;
 
    explicit destructor_nodet(codet destructor)
      : destructor_value(std::move(destructor))
    {
    }
    optionalt<codet> destructor_value;
  };
 
  grapht<destructor_nodet> destruction_graph;
  node_indext current_node = 0;
};
 
#endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_TREE_H