cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
ansi_c_declaration.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: ANSI-C Language Type Checking
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
ansi_c_declaration.h
"
13
14
#include <ostream>
15
16
#include <
util/config.h
>
17
#include <
util/invariant.h
>
18
#include <
util/std_types.h
>
19
#include <
util/symbol.h
>
20
21
#include "
merged_type.h
"
22
23
void
ansi_c_declaratort::build
(
irept
&src)
24
{
25
typet
*p=
static_cast<
typet
*
>
(&src);
26
27
// walk down subtype until we hit typedef_type, symbol or "abstract"
28
while
(
true
)
29
{
30
typet
&t=*p;
31
32
if
(t.
id
() == ID_typedef_type || t.
id
() == ID_symbol)
33
{
34
set_base_name
(t.
get
(ID_C_base_name));
35
add_source_location
()=t.
source_location
();
36
t.
make_nil
();
37
break
;
38
}
39
else
if
(t.
id
().
empty
() ||
40
t.
is_nil
())
41
{
42
UNREACHABLE
;
43
}
44
else
if
(t.
id
()==ID_abstract)
45
{
46
t.
make_nil
();
47
break
;
48
}
49
else
if
(t.
id
()==ID_merged_type)
50
{
51
// we always walk down the _last_ member of a merged type
52
auto
&merged_type =
to_merged_type
(t);
53
p = &merged_type.last_type();
54
}
55
else
56
p = &t.
add_subtype
();
57
}
58
59
type
()=
static_cast<
const
typet
&
>
(src);
60
value
().
make_nil
();
61
}
62
63
void
ansi_c_declarationt::output
(std::ostream &out)
const
64
{
65
out <<
"Flags:"
;
66
if
(
get_is_typedef
())
67
out <<
" is_typedef"
;
68
if
(
get_is_enum_constant
())
69
out <<
" is_enum_constant"
;
70
if
(
get_is_static
())
71
out <<
" is_static"
;
72
if
(
get_is_parameter
())
73
out <<
" is_parameter"
;
74
if
(
get_is_global
())
75
out <<
" is_global"
;
76
if
(
get_is_register
())
77
out <<
" is_register"
;
78
if
(
get_is_thread_local
())
79
out <<
" is_thread_local"
;
80
if
(
get_is_inline
())
81
out <<
" is_inline"
;
82
if
(
get_is_extern
())
83
out <<
" is_extern"
;
84
if
(
get_is_static_assert
())
85
out <<
" is_static_assert"
;
86
out <<
"\n"
;
87
88
out <<
"Type: "
<<
type
().
pretty
() <<
"\n"
;
89
90
for
(
const
auto
&
declarator
:
declarators
())
91
out <<
"Declarator: "
<<
declarator
.pretty() <<
"\n"
;
92
}
93
94
typet
ansi_c_declarationt::full_type
(
95
const
ansi_c_declaratort
&
declarator
)
const
96
{
97
typet
result=
declarator
.type();
98
typet
*p=&result;
99
100
// this gets types that are still raw parse trees
101
while
(p->
is_not_nil
())
102
{
103
if
(p->
id
()==ID_frontend_pointer || p->
id
()==ID_array ||
104
p->
id
()==ID_vector || p->
id
()==ID_c_bit_field ||
105
p->
id
()==ID_block_pointer || p->
id
()==ID_code)
106
{
107
p = &p->
add_subtype
();
108
}
109
else
if
(p->
id
()==ID_merged_type)
110
{
111
// we always go down on the right-most subtype
112
auto
&merged_type =
to_merged_type
(*p);
113
p = &merged_type.last_type();
114
}
115
else
116
UNREACHABLE
;
117
}
118
119
*p=
type
();
120
121
// retain typedef for dump-c
122
if
(
get_is_typedef
())
123
result.
set
(ID_C_typedef,
declarator
.get_name());
124
125
return
result;
126
}
127
128
symbolt
129
ansi_c_declarationt::to_symbol
(
const
ansi_c_declaratort
&
declarator
)
const
130
{
131
symbolt
symbol{
declarator
.get_name(),
full_type
(
declarator
), ID_C};
132
symbol.
value
=
declarator
.value();
133
symbol.
pretty_name
=symbol.
name
;
134
symbol.
base_name
=
declarator
.get_base_name();
135
symbol.
is_type
=
get_is_typedef
();
136
symbol.
location
=
declarator
.source_location();
137
symbol.
is_extern
=
get_is_extern
();
138
symbol.
is_macro
=
get_is_typedef
() ||
get_is_enum_constant
();
139
symbol.
is_parameter
=
get_is_parameter
();
140
symbol.
is_weak
=
get_is_weak
();
141
142
// is it a function?
143
typet
&
type
= symbol.
type
.
id
() == ID_merged_type
144
?
to_merged_type
(symbol.
type
).
last_type
()
145
: symbol.
type
;
146
147
if
(
type
.id() == ID_code && !symbol.
is_type
)
148
{
149
symbol.
is_static_lifetime
=
false
;
150
symbol.
is_thread_local
=
false
;
151
152
symbol.
is_file_local
=
get_is_static
();
153
154
if
(
get_is_inline
())
155
to_code_type
(
type
).
set_inlined
(
true
);
156
157
if
(
158
config
.ansi_c.mode ==
configt::ansi_ct::flavourt::GCC
||
159
config
.ansi_c.mode ==
configt::ansi_ct::flavourt::CLANG
||
160
config
.ansi_c.mode ==
configt::ansi_ct::flavourt::ARM
)
161
{
162
// GCC extern inline cleanup, to enable remove_internal_symbols
163
// do its full job
164
// https://gcc.gnu.org/ml/gcc/2006-11/msg00006.html
165
// __attribute__((__gnu_inline__))
166
if
(
get_is_inline
())
167
{
168
if
(
get_is_static
())
// C99 and above
169
symbol.
is_extern
=
false
;
170
else
if
(
get_is_extern
())
// traditional GCC
171
symbol.
is_file_local
=
true
;
172
}
173
}
174
}
175
else
// non-function
176
{
177
symbol.
is_static_lifetime
=
178
!symbol.
is_macro
&&
179
!symbol.
is_type
&&
180
(
get_is_global
() ||
get_is_static
());
181
182
symbol.
is_thread_local
=
183
(!symbol.
is_static_lifetime
&& !
get_is_extern
()) ||
184
get_is_thread_local
();
185
186
symbol.
is_file_local
=
187
symbol.
is_macro
|| (!
get_is_global
() && !
get_is_extern
()) ||
188
(
get_is_global
() &&
get_is_static
()) || symbol.
is_parameter
;
189
}
190
191
return
symbol;
192
}
ansi_c_declaration.h
ANSI-CC Language Type Checking.
config
configt config
Definition
config.cpp:25
ansi_c_declarationt::declarator
const ansi_c_declaratort & declarator() const
Definition
ansi_c_declaration.h:215
ansi_c_declarationt::to_symbol
symbolt to_symbol(const ansi_c_declaratort &) const
Definition
ansi_c_declaration.cpp:129
ansi_c_declarationt::get_is_extern
bool get_is_extern() const
Definition
ansi_c_declaration.h:168
ansi_c_declarationt::declarators
const declaratorst & declarators() const
Definition
ansi_c_declaration.h:204
ansi_c_declarationt::get_is_parameter
bool get_is_parameter() const
Definition
ansi_c_declaration.h:108
ansi_c_declarationt::get_is_inline
bool get_is_inline() const
Definition
ansi_c_declaration.h:158
ansi_c_declarationt::full_type
typet full_type(const ansi_c_declaratort &) const
Definition
ansi_c_declaration.cpp:94
ansi_c_declarationt::get_is_enum_constant
bool get_is_enum_constant() const
Definition
ansi_c_declaration.h:88
ansi_c_declarationt::get_is_static
bool get_is_static() const
Definition
ansi_c_declaration.h:98
ansi_c_declarationt::get_is_register
bool get_is_register() const
Definition
ansi_c_declaration.h:138
ansi_c_declarationt::get_is_global
bool get_is_global() const
Definition
ansi_c_declaration.h:128
ansi_c_declarationt::get_is_thread_local
bool get_is_thread_local() const
Definition
ansi_c_declaration.h:148
ansi_c_declarationt::get_is_typedef
bool get_is_typedef() const
Definition
ansi_c_declaration.h:78
ansi_c_declarationt::get_is_weak
bool get_is_weak() const
Definition
ansi_c_declaration.h:188
ansi_c_declarationt::get_is_static_assert
bool get_is_static_assert() const
Definition
ansi_c_declaration.h:178
ansi_c_declarationt::output
void output(std::ostream &) const
Definition
ansi_c_declaration.cpp:63
ansi_c_declaratort
Definition
ansi_c_declaration.h:20
ansi_c_declaratort::set_base_name
void set_base_name(const irep_idt &base_name)
Definition
ansi_c_declaration.h:51
ansi_c_declaratort::build
void build(irept &src)
Definition
ansi_c_declaration.cpp:23
ansi_c_declaratort::value
exprt & value()
Definition
ansi_c_declaration.h:26
code_typet::set_inlined
void set_inlined(bool value)
Definition
std_types.h:714
dstringt::empty
bool empty() const
Definition
dstring.h:89
exprt::type
typet & type()
Return the type of the expression.
Definition
expr.h:85
exprt::add_source_location
source_locationt & add_source_location()
Definition
expr.h:241
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition
irep.h:364
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition
irep.cpp:482
irept::get
const irep_idt & get(const irep_idt &name) const
Definition
irep.cpp:44
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition
irep.h:412
irept::is_not_nil
bool is_not_nil() const
Definition
irep.h:372
irept::make_nil
void make_nil()
Definition
irep.h:446
irept::id
const irep_idt & id() const
Definition
irep.h:388
irept::is_nil
bool is_nil() const
Definition
irep.h:368
merged_typet::last_type
typet & last_type()
Definition
merged_type.h:22
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition
symbol.h:46
symbolt::is_extern
bool is_extern
Definition
symbol.h:74
symbolt::is_macro
bool is_macro
Definition
symbol.h:62
symbolt::is_file_local
bool is_file_local
Definition
symbol.h:73
symbolt::is_static_lifetime
bool is_static_lifetime
Definition
symbol.h:70
symbolt::is_parameter
bool is_parameter
Definition
symbol.h:76
symbolt::is_thread_local
bool is_thread_local
Definition
symbol.h:71
symbolt::is_type
bool is_type
Definition
symbol.h:61
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition
symbol.h:37
symbolt::type
typet type
Type of symbol.
Definition
symbol.h:31
symbolt::is_weak
bool is_weak
Definition
symbol.h:78
symbolt::name
irep_idt name
The unique identifier.
Definition
symbol.h:40
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition
symbol.h:52
symbolt::value
exprt value
Initial value of symbol.
Definition
symbol.h:34
typet
The type of an expression, extends irept.
Definition
type.h:29
typet::source_location
const source_locationt & source_location() const
Definition
type.h:72
typet::add_subtype
typet & add_subtype()
Definition
type.h:53
config.h
merged_type.h
to_merged_type
const merged_typet & to_merged_type(const typet &type)
conversion to merged_typet
Definition
merged_type.h:29
invariant.h
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition
invariant.h:525
std_types.h
Pre-defined types.
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition
std_types.h:788
configt::ansi_ct::flavourt::GCC
@ GCC
Definition
config.h:274
configt::ansi_ct::flavourt::ARM
@ ARM
Definition
config.h:275
configt::ansi_ct::flavourt::CLANG
@ CLANG
Definition
config.h:276
symbol.h
Symbol table entry.
ansi-c
ansi_c_declaration.cpp
Generated by
1.17.0