Skip to content

Commit c66d099

Browse files
author
Daniel Kroening
committed
added class_hierarchy analysis
1 parent af9ac28 commit c66d099

File tree

2 files changed

+141
-0
lines changed

2 files changed

+141
-0
lines changed

src/goto-programs/class_hierarchy.cpp

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
/*******************************************************************\
2+
3+
Module: Class Hierarchy
4+
5+
Author: Daniel Kroening
6+
7+
Date: April 2016
8+
9+
\*******************************************************************/
10+
11+
#include <util/std_types.h>
12+
13+
#include "class_hierarchy.h"
14+
15+
/*******************************************************************\
16+
17+
Function: class_hierarchyt::operator()
18+
19+
Inputs:
20+
21+
Outputs:
22+
23+
Purpose:
24+
25+
\*******************************************************************/
26+
27+
void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
28+
{
29+
forall_symbols(it, symbol_table.symbols)
30+
{
31+
if(it->second.is_type && it->second.type.id()==ID_struct)
32+
{
33+
const struct_typet &struct_type=
34+
to_struct_type(it->second.type);
35+
36+
const struct_typet::componentst &components=
37+
struct_type.components();
38+
39+
if(components.empty()) continue;
40+
41+
irep_idt name=components.front().get_name();
42+
43+
if(name.empty()) continue;
44+
45+
if(name[0]!='@') continue;
46+
47+
if(components.front().type().id()!=ID_symbol) continue;
48+
49+
irep_idt parent=
50+
to_symbol_type(components.front().type()).get_identifier();
51+
52+
class_map[parent].children.push_back(it->first);
53+
class_map[it->first].parent=parent;
54+
}
55+
}
56+
}
57+
58+
/*******************************************************************\
59+
60+
Function: class_hierarchyt::get_children
61+
62+
Inputs:
63+
64+
Outputs:
65+
66+
Purpose:
67+
68+
\*******************************************************************/
69+
70+
void class_hierarchyt::get_children(
71+
const irep_idt &c,
72+
std::vector<irep_idt> &dest) const
73+
{
74+
class_mapt::const_iterator it=class_map.find(c);
75+
if(it==class_map.end()) return;
76+
const entryt &entry=it->second;
77+
78+
for(const auto & child : entry.children)
79+
dest.push_back(child);
80+
81+
// recursive calls
82+
for(const auto & child : entry.children)
83+
get_children(child, dest);
84+
}
85+
86+
/*******************************************************************\
87+
88+
Function: class_hierarchyt::get_parent
89+
90+
Inputs:
91+
92+
Outputs:
93+
94+
Purpose:
95+
96+
\*******************************************************************/
97+
98+
irep_idt class_hierarchyt::get_parent(const irep_idt &c) const
99+
{
100+
class_mapt::const_iterator it=class_map.find(c);
101+
if(it==class_map.end()) return irep_idt();
102+
return it->second.parent;
103+
}

src/goto-programs/class_hierarchy.h

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
/*******************************************************************\
2+
3+
Module: Class Hierarchy
4+
5+
Author: Daniel Kroening
6+
7+
Date: April 2016
8+
9+
\*******************************************************************/
10+
11+
#ifndef CPROVER_CLASS_HIERARCHY_H
12+
#define CPROVER_CLASS_HIERARCHY_H
13+
14+
#include <util/symbol_table.h>
15+
16+
class class_hierarchyt
17+
{
18+
public:
19+
class entryt
20+
{
21+
public:
22+
irep_idt parent;
23+
typedef std::vector<irep_idt> childrent;
24+
childrent children;
25+
};
26+
27+
typedef std::map<irep_idt, entryt> class_mapt;
28+
class_mapt class_map;
29+
30+
void operator()(const symbol_tablet &);
31+
32+
// transitively gets all children
33+
void get_children(const irep_idt &, std::vector<irep_idt> &) const;
34+
35+
irep_idt get_parent(const irep_idt &) const;
36+
};
37+
38+
#endif

0 commit comments

Comments
 (0)