cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
cpp_scopes.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: C++ Language Type Checking
4
5
Author: Daniel Kroening, kroening@cs.cmu.edu
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_CPP_CPP_SCOPES_H
13
#define CPROVER_CPP_CPP_SCOPES_H
14
15
#include <set>
16
17
#include "
cpp_scope.h
"
18
19
class
symbolt
;
20
21
class
cpp_scopest
22
{
23
public
:
24
cpp_scopest
()
25
{
26
current_scope_ptr
=&
root_scope
;
27
}
28
29
typedef
std::set<cpp_scopet *>
scope_sett
;
30
typedef
std::set<cpp_idt *>
id_sett
;
31
32
cpp_scopet
&
current_scope
()
33
{
34
return
*
current_scope_ptr
;
35
}
36
37
cpp_scopet
&
new_scope
(
38
const
irep_idt
&new_scope_name,
39
cpp_idt::id_classt
id_class
)
40
{
41
PRECONDITION
(!new_scope_name.
empty
());
42
cpp_scopet
&n=
current_scope_ptr
->new_scope(new_scope_name);
43
n.
id_class
=
id_class
;
44
id_map
[n.
identifier
]=&n;
45
current_scope_ptr
=&n;
46
return
n;
47
}
48
49
cpp_scopet
&
new_namespace
(
const
irep_idt
&new_scope_name)
50
{
51
return
new_scope
(new_scope_name,
cpp_idt::id_classt::NAMESPACE
);
52
}
53
54
cpp_scopet
&
new_block_scope
();
55
56
cpp_idt
&
put_into_scope
(
57
const
symbolt
&symbol,
58
cpp_scopet
&scope,
59
bool
is_friend =
false
);
60
61
cpp_idt
&
put_into_scope
(
const
symbolt
&symbol,
bool
is_friend =
false
)
62
{
63
return
put_into_scope
(symbol,
current_scope
(), is_friend);
64
}
65
66
// mapping from function/class/scope names to their cpp_idt
67
typedef
std::unordered_map<irep_idt, cpp_idt *>
id_mapt
;
68
id_mapt
id_map
;
69
70
cpp_scopet
*
current_scope_ptr
;
71
72
cpp_idt
&
get_id
(
const
irep_idt
&identifier)
73
{
74
id_mapt::const_iterator it=
id_map
.find(identifier);
75
if
(it==
id_map
.end())
76
throw
"id '"
+
id2string
(identifier) +
"' not found"
;
77
return
*(it->second);
78
}
79
80
cpp_scopet
&
get_scope
(
const
irep_idt
&identifier)
81
{
82
cpp_idt
&n=
get_id
(identifier);
83
CHECK_RETURN
(n.
is_scope
);
84
return
(
cpp_scopet
&)n;
85
}
86
87
cpp_scopet
&
set_scope
(
const
irep_idt
&identifier)
88
{
89
current_scope_ptr
=&
get_scope
(identifier);
90
return
current_scope
();
91
}
92
93
cpp_scopet
&
get_root_scope
()
94
{
95
return
root_scope
;
96
}
97
98
void
go_to_root_scope
()
99
{
100
current_scope_ptr
=&
root_scope
;
101
}
102
103
void
go_to
(
cpp_idt
&
id
)
104
{
105
PRECONDITION
(
id
.is_scope);
106
current_scope_ptr
=
static_cast<
cpp_scopet
*
>
(&id);
107
}
108
109
// move up to next global scope
110
void
go_to_global_scope
()
111
{
112
current_scope_ptr
=&
get_global_scope
();
113
}
114
115
cpp_scopet
&
get_global_scope
()
116
{
117
return
current_scope
().
get_global_scope
();
118
}
119
120
void
print_current
(std::ostream &out)
const
;
121
122
protected
:
123
// the root scope
124
cpp_root_scopet
root_scope
;
125
};
126
127
class
cpp_save_scopet
128
{
129
public
:
130
explicit
cpp_save_scopet
(
cpp_scopest
&_cpp_scopes):
131
cpp_scopes
(_cpp_scopes),
132
saved_scope
(_cpp_scopes.current_scope_ptr)
133
{
134
}
135
136
~cpp_save_scopet
()
137
{
138
restore
();
139
}
140
141
void
restore
()
142
{
143
cpp_scopes
.current_scope_ptr=
saved_scope
;
144
}
145
146
protected
:
147
cpp_scopest
&
cpp_scopes
;
148
cpp_scopet
*
saved_scope
;
149
};
150
151
#endif
// CPROVER_CPP_CPP_SCOPES_H
cpp_idt
Definition
cpp_id.h:23
cpp_idt::identifier
irep_idt identifier
Definition
cpp_id.h:72
cpp_idt::is_scope
bool is_scope
Definition
cpp_id.h:43
cpp_idt::id_classt
id_classt
Definition
cpp_id.h:28
cpp_idt::id_classt::NAMESPACE
@ NAMESPACE
Definition
cpp_id.h:36
cpp_idt::id_class
id_classt id_class
Definition
cpp_id.h:45
cpp_root_scopet
Definition
cpp_scope.h:128
cpp_save_scopet::saved_scope
cpp_scopet * saved_scope
Definition
cpp_scopes.h:148
cpp_save_scopet::~cpp_save_scopet
~cpp_save_scopet()
Definition
cpp_scopes.h:136
cpp_save_scopet::restore
void restore()
Definition
cpp_scopes.h:141
cpp_save_scopet::cpp_scopes
cpp_scopest & cpp_scopes
Definition
cpp_scopes.h:147
cpp_save_scopet::cpp_save_scopet
cpp_save_scopet(cpp_scopest &_cpp_scopes)
Definition
cpp_scopes.h:130
cpp_scopest
Definition
cpp_scopes.h:22
cpp_scopest::go_to_root_scope
void go_to_root_scope()
Definition
cpp_scopes.h:98
cpp_scopest::go_to
void go_to(cpp_idt &id)
Definition
cpp_scopes.h:103
cpp_scopest::print_current
void print_current(std::ostream &out) const
Definition
cpp_scopes.cpp:72
cpp_scopest::cpp_scopest
cpp_scopest()
Definition
cpp_scopes.h:24
cpp_scopest::get_id
cpp_idt & get_id(const irep_idt &identifier)
Definition
cpp_scopes.h:72
cpp_scopest::new_block_scope
cpp_scopet & new_block_scope()
Definition
cpp_scopes.cpp:18
cpp_scopest::current_scope_ptr
cpp_scopet * current_scope_ptr
Definition
cpp_scopes.h:70
cpp_scopest::id_mapt
std::unordered_map< irep_idt, cpp_idt * > id_mapt
Definition
cpp_scopes.h:67
cpp_scopest::scope_sett
std::set< cpp_scopet * > scope_sett
Definition
cpp_scopes.h:29
cpp_scopest::id_sett
std::set< cpp_idt * > id_sett
Definition
cpp_scopes.h:30
cpp_scopest::put_into_scope
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition
cpp_scopes.cpp:24
cpp_scopest::new_scope
cpp_scopet & new_scope(const irep_idt &new_scope_name, cpp_idt::id_classt id_class)
Definition
cpp_scopes.h:37
cpp_scopest::new_namespace
cpp_scopet & new_namespace(const irep_idt &new_scope_name)
Definition
cpp_scopes.h:49
cpp_scopest::id_map
id_mapt id_map
Definition
cpp_scopes.h:68
cpp_scopest::put_into_scope
cpp_idt & put_into_scope(const symbolt &symbol, bool is_friend=false)
Definition
cpp_scopes.h:61
cpp_scopest::get_global_scope
cpp_scopet & get_global_scope()
Definition
cpp_scopes.h:115
cpp_scopest::get_scope
cpp_scopet & get_scope(const irep_idt &identifier)
Definition
cpp_scopes.h:80
cpp_scopest::set_scope
cpp_scopet & set_scope(const irep_idt &identifier)
Definition
cpp_scopes.h:87
cpp_scopest::root_scope
cpp_root_scopet root_scope
Definition
cpp_scopes.h:124
cpp_scopest::go_to_global_scope
void go_to_global_scope()
Definition
cpp_scopes.h:110
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition
cpp_scopes.h:32
cpp_scopest::get_root_scope
cpp_scopet & get_root_scope()
Definition
cpp_scopes.h:93
cpp_scopet
Definition
cpp_scope.h:21
cpp_scopet::get_global_scope
cpp_scopet & get_global_scope()
Definition
cpp_scope.h:93
dstringt::empty
bool empty() const
Definition
dstring.h:89
symbolt
Symbol table entry.
Definition
symbol.h:28
cpp_scope.h
C++ Language Type Checking.
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
idt::id_class
@ id_class
Definition
irep_ids.cpp:181
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition
invariant.h:495
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
cpp
cpp_scopes.h
Generated by
1.17.0