cprover
Loading...
Searching...
No Matches
class_hierarchy.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Class Hierarchy
4
5Author: Daniel Kroening
6
7Date: 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
24// clang-format off
25#define OPT_SHOW_CLASS_HIERARCHY \
26 "(show-class-hierarchy)"
27
28#define HELP_SHOW_CLASS_HIERARCHY \
29 " --show-class-hierarchy show the class hierarchy\n"
30// clang-format on
31
32class symbol_tablet;
35
43{
44public:
45 typedef std::vector<irep_idt> idst;
46
47 class entryt
48 {
49 public:
52 };
53
54 typedef std::map<irep_idt, entryt> class_mapt;
56
57 void operator()(const symbol_tablet &);
58
59 class_hierarchyt() = default;
60 explicit class_hierarchyt(const symbol_tablet &symbol_table)
61 {
62 (*this)(symbol_table);
63 }
66
67 // transitively gets all children
69 {
70 idst result;
71 get_children_trans_rec(id, result);
72 return result;
73 }
74
75 // transitively gets all parents
77 {
78 idst result;
79 get_parents_trans_rec(id, result);
80 return result;
81 }
82
83 void output(std::ostream &, bool children_only) const;
84 void output_dot(std::ostream &) const;
85 void output(json_stream_arrayt &, bool children_only) const;
86
87protected:
88 void get_children_trans_rec(const irep_idt &, idst &) const;
89 void get_parents_trans_rec(const irep_idt &, idst &) const;
90};
91
93class class_hierarchy_graph_nodet : public graph_nodet<empty_edget>
94{
95public:
98};
99
102class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
103{
104public:
105 typedef std::vector<irep_idt> idst;
106
108 typedef std::unordered_map<irep_idt, node_indext> nodes_by_namet;
109
110 void populate(const symbol_tablet &);
111
115 {
116 return nodes_by_name;
117 }
118
119 idst get_direct_children(const irep_idt &c) const;
120
121 idst get_children_trans(const irep_idt &c) const;
122
123 idst get_parents_trans(const irep_idt &c) const;
124
125private:
128
129 idst ids_from_indices(const std::vector<node_indext> &nodes) const;
130
131 idst get_other_reachable_ids(const irep_idt &c, bool forwards) const;
132};
133
139 const class_hierarchyt &hierarchy,
140 ui_message_handlert &message_handler,
141 bool children_only = false);
142
143#endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only=false)
Output the class hierarchy.
Class hierarchy graph node: simply contains a class identifier.
irep_idt class_identifier
Class ID for this node.
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
std::unordered_map< irep_idt, node_indext > nodes_by_namet
Maps class identifiers onto node indices.
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.
idst get_children_trans(const irep_idt &c) const
Get all the classes that inherit (directly or indirectly) from class c.
std::vector< irep_idt > idst
const nodes_by_namet & get_nodes_by_class_identifier() const
Get map from class identifier to node index.
idst get_direct_children(const irep_idt &c) const
Get all the classes that directly (i.e.
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).
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...
Non-graph-based representation of the class hierarchy.
idst get_parents_trans(const irep_idt &id) const
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
void get_parents_trans_rec(const irep_idt &, idst &) const
Get all the classes that class c inherits from (directly or indirectly).
class_hierarchyt(const symbol_tablet &symbol_table)
class_hierarchyt & operator=(const class_hierarchyt &)=delete
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...
class_mapt class_map
std::map< irep_idt, entryt > class_mapt
class_hierarchyt()=default
void get_children_trans_rec(const irep_idt &, idst &) const
idst get_children_trans(const irep_idt &id) const
void output(std::ostream &, bool children_only) const
Output the class hierarchy in plain text.
class_hierarchyt(const class_hierarchyt &)=delete
std::vector< irep_idt > idst
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
This class represents a node in a directed graph.
Definition: graph.h:35
A generic directed graph with a parametric node type.
Definition: graph.h:167
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
The symbol table.
Definition: symbol_table.h:14
A Template Class for Graphs.