cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
cpp_scopes.cpp
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
#include "
cpp_scopes.h
"
13
14
#include <
util/symbol.h
>
15
16
#include <ostream>
17
18
cpp_scopet
&
cpp_scopest::new_block_scope
()
19
{
20
unsigned
prefix=++
current_scope
().
compound_counter
;
21
return
new_scope
(std::to_string(prefix),
cpp_idt::id_classt::BLOCK_SCOPE
);
22
}
23
24
cpp_idt
&
cpp_scopest::put_into_scope
(
25
const
symbolt
&symbol,
26
cpp_scopet
&scope,
27
bool
is_friend)
28
{
29
PRECONDITION
(!symbol.
name
.
empty
());
30
PRECONDITION
(!symbol.
base_name
.
empty
());
31
32
// functions are also scopes
33
if
(symbol.
type
.
id
()==ID_code)
34
{
35
cpp_scopest::id_mapt::iterator id_it =
id_map
.find(symbol.
name
);
36
if
(id_it ==
id_map
.end())
37
{
38
irep_idt
block_base_name(std::string(
"$block:"
)+symbol.
base_name
.
c_str
());
39
cpp_idt
&
id
= scope.
insert
(block_base_name);
40
id
.
id_class
=
cpp_idt::id_classt::BLOCK_SCOPE
;
41
id
.identifier=symbol.
name
;
42
id
.is_scope=
true
;
43
id
.prefix =
id2string
(scope.
prefix
) +
id2string
(symbol.
base_name
) +
"::"
;
44
id_map
[symbol.
name
]=&id;
45
}
46
}
47
48
// should go away, and be replaced by the 'tag only declaration' rule
49
if
(is_friend)
50
{
51
cpp_save_scopet
saved_scope(*
this
);
52
go_to
(scope);
53
54
cpp_idt
&
id
=
current_scope
().
insert
(symbol.
base_name
);
55
id
.
identifier
=symbol.
name
;
56
id
.id_class =
cpp_idt::id_classt::SYMBOL
;
57
if
(
id_map
.find(symbol.
name
)==
id_map
.end())
58
id_map
[symbol.
name
]=&id;
59
return
id;
60
}
61
else
62
{
63
cpp_idt
&
id
=scope.
insert
(symbol.
base_name
);
64
id
.
identifier
=symbol.
name
;
65
id
.id_class =
cpp_idt::id_classt::SYMBOL
;
66
if
(
id_map
.find(symbol.
name
)==
id_map
.end())
67
id_map
[symbol.
name
]=&id;
68
return
id;
69
}
70
}
71
72
void
cpp_scopest::print_current
(std::ostream &out)
const
73
{
74
const
cpp_scopet
*scope=
current_scope_ptr
;
75
76
do
77
{
78
scope->
print_fields
(out);
79
out <<
'\n'
;
80
scope=&scope->
get_parent
();
81
}
82
while
(!scope->
is_root_scope
());
83
}
cpp_idt
Definition
cpp_id.h:23
cpp_idt::identifier
irep_idt identifier
Definition
cpp_id.h:72
cpp_idt::prefix
std::string prefix
Definition
cpp_id.h:79
cpp_idt::id_classt::BLOCK_SCOPE
@ BLOCK_SCOPE
Definition
cpp_id.h:37
cpp_idt::id_classt::SYMBOL
@ SYMBOL
Definition
cpp_id.h:30
cpp_idt::id_class
id_classt id_class
Definition
cpp_id.h:45
cpp_idt::print_fields
void print_fields(std::ostream &out, unsigned indent=0) const
Definition
cpp_id.cpp:44
cpp_idt::compound_counter
unsigned compound_counter
Definition
cpp_id.h:80
cpp_save_scopet
Definition
cpp_scopes.h:128
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::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::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::id_map
id_mapt id_map
Definition
cpp_scopes.h:68
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition
cpp_scopes.h:32
cpp_scopet
Definition
cpp_scope.h:21
cpp_scopet::get_parent
cpp_scopet & get_parent() const
Definition
cpp_scope.h:88
cpp_scopet::insert
cpp_idt & insert(const irep_idt &_base_name)
Definition
cpp_scope.h:52
cpp_scopet::is_root_scope
bool is_root_scope() const
Definition
cpp_scope.h:77
dstringt::empty
bool empty() const
Definition
dstring.h:89
dstringt::c_str
const char * c_str() const
Definition
dstring.h:116
irept::id
const irep_idt & id() const
Definition
irep.h:388
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition
symbol.h:46
symbolt::type
typet type
Type of symbol.
Definition
symbol.h:31
symbolt::name
irep_idt name
The unique identifier.
Definition
symbol.h:40
cpp_scopes.h
C++ Language Type Checking.
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
symbol.h
Symbol table entry.
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
cpp
cpp_scopes.cpp
Generated by
1.17.0