cprover
class_hierarchy.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Class Hierarchy
4 
5 Author: Daniel Kroening
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H
15 #define CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H
16 
17 #include <iosfwd>
18 #include <map>
19 #include <unordered_map>
20 
21 #include <util/graph.h>
22 #include <util/irep.h>
23 #include <util/ui_message.h>
24 
25 // clang-format off
26 #define OPT_SHOW_CLASS_HIERARCHY \
27  "(show-class-hierarchy)"
28 
29 #define HELP_SHOW_CLASS_HIERARCHY \
30  " --show-class-hierarchy show the class hierarchy\n"
31 // clang-format on
32 
33 class symbol_tablet;
34 class json_stream_arrayt;
35 class message_handlert;
36 
44 {
45 public:
46  typedef std::vector<irep_idt> idst;
47 
48  class entryt
49  {
50  public:
53  };
54 
55  typedef std::map<irep_idt, entryt> class_mapt;
57 
58  void operator()(const symbol_tablet &);
59 
60  // transitively gets all children
61  idst get_children_trans(const irep_idt &id) const
62  {
63  idst result;
64  get_children_trans_rec(id, result);
65  return result;
66  }
67 
68  // transitively gets all parents
69  idst get_parents_trans(const irep_idt &id) const
70  {
71  idst result;
72  get_parents_trans_rec(id, result);
73  return result;
74  }
75 
76  void output(std::ostream &, bool children_only) const;
77  void output_dot(std::ostream &) const;
78  void output(json_stream_arrayt &, bool children_only) const;
79 
80 protected:
81  void get_children_trans_rec(const irep_idt &, idst &) const;
82  void get_parents_trans_rec(const irep_idt &, idst &) const;
83 };
84 
86 class class_hierarchy_graph_nodet : public graph_nodet<empty_edget>
87 {
88 public:
91 };
92 
95 class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
96 {
97 public:
98  typedef std::vector<irep_idt> idst;
99 
101  typedef std::unordered_map<irep_idt, node_indext> nodes_by_namet;
102 
103  void populate(const symbol_tablet &);
104 
108  {
109  return nodes_by_name;
110  }
111 
112  idst get_direct_children(const irep_idt &c) const;
113 
114  idst get_children_trans(const irep_idt &c) const;
115 
116  idst get_parents_trans(const irep_idt &c) const;
117 
118 private:
121 
122  idst ids_from_indices(const std::vector<node_indext> &nodes) const;
123 
124  idst get_other_reachable_ids(const irep_idt &c, bool forwards) const;
125 };
126 
133  const class_hierarchyt &hierarchy,
136  bool children_only = false);
137 
138 #endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H
A generic directed graph with a parametric node type.
Definition: graph.h:133
idst ids_from_indices(const std::vector< node_indext > &nodes) const
Helper function that converts a vector of node_indext to a vector of ids that are stored in the corre...
void get_children_trans_rec(const irep_idt &, idst &) const
void operator()(const symbol_tablet &)
Looks for all the struct types in the symbol table and construct a map from class names to a data str...
std::unordered_map< irep_idt, node_indext > nodes_by_namet
Maps class identifiers onto node indices.
void output(std::ostream &, bool children_only) const
Output the class hierarchy in plain text.
Non-graph-based representation of the class hierarchy.
void show_class_hierarchy(const class_hierarchyt &hierarchy, message_handlert &message_handler, ui_message_handlert::uit ui, bool children_only=false)
Output the class hierarchy.
void populate(const symbol_tablet &)
Populate the class hierarchy graph, such that there is a node for every struct type in the symbol tab...
nodes_by_namet nodes_by_name
Maps class identifiers onto node indices.
void get_parents_trans_rec(const irep_idt &, idst &) const
Get all the classes that class c inherits from (directly or indirectly).
idst get_children_trans(const irep_idt &c) const
Get all the classes that inherit (directly or indirectly) from class c.
idst get_direct_children(const irep_idt &c) const
Get all the classes that directly (i.e.
irep_idt class_identifier
Class ID for this node.
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
The symbol table.
Definition: symbol_table.h:19
Provides methods for streaming JSON arrays.
Definition: json_stream.h:92
class_mapt class_map
const nodes_by_namet & get_nodes_by_class_identifier() const
Get map from class identifier to node index.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::vector< irep_idt > idst
A Template Class for Graphs.
std::vector< irep_idt > idst
std::map< irep_idt, entryt > class_mapt
idst get_other_reachable_ids(const irep_idt &c, bool forwards) const
Helper function for get_children_trans and get_parents_trans
idst get_parents_trans(const irep_idt &c) const
Get all the classes that class c inherits from (directly or indirectly).
Class hierarchy graph node: simply contains a class identifier.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
idst get_children_trans(const irep_idt &id) const
This class represents a node in a directed graph.
Definition: graph.h:34
idst get_parents_trans(const irep_idt &id) const