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 
38 {
39 public:
40  typedef std::vector<irep_idt> idst;
41 
42  class entryt
43  {
44  public:
47  };
48 
49  typedef std::map<irep_idt, entryt> class_mapt;
51 
52  void operator()(const symbol_tablet &);
53 
54  // transitively gets all children
55  idst get_children_trans(const irep_idt &id) const
56  {
57  idst result;
58  get_children_trans_rec(id, result);
59  return result;
60  }
61 
62  // transitively gets all parents
63  idst get_parents_trans(const irep_idt &id) const
64  {
65  idst result;
66  get_parents_trans_rec(id, result);
67  return result;
68  }
69 
70  void output(std::ostream &, bool children_only) const;
71  void output_dot(std::ostream &) const;
72  void output(json_stream_arrayt &, bool children_only) const;
73 
74 protected:
75  void get_children_trans_rec(const irep_idt &, idst &) const;
76  void get_parents_trans_rec(const irep_idt &, idst &) const;
77 };
78 
80 class class_hierarchy_graph_nodet : public graph_nodet<empty_edget>
81 {
82 public:
85 };
86 
89 class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
90 {
91 public:
93  typedef std::unordered_map<irep_idt, node_indext> nodes_by_namet;
94 
95  void populate(const symbol_tablet &);
96 
100  {
101  return nodes_by_name;
102  }
103 
104 private:
107 };
108 
115  const class_hierarchyt &hierarchy,
118  bool children_only = false);
119 
120 #endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H
A generic directed graph with a parametric node type.
Definition: graph.h:133
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.
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 inherit (directly or indirectly) from class c.
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.
std::vector< irep_idt > idst
A Template Class for Graphs.
std::map< irep_idt, entryt > class_mapt
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