CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
ansi_c_declaration.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-CC Language Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANSI_C_ANSI_C_DECLARATION_H
13#define CPROVER_ANSI_C_ANSI_C_DECLARATION_H
14
15#include <util/std_expr.h>
16
17class symbolt;
18
20{
21public:
25
27 {
28 return static_cast<exprt &>(add(ID_value));
29 }
30
31 const exprt &value() const
32 {
33 return static_cast<const exprt &>(find(ID_value));
34 }
35
36 void set_name(const irep_idt &name)
37 {
38 return set(ID_name, name);
39 }
40
42 {
43 return get(ID_name);
44 }
45
47 {
48 return get(ID_base_name);
49 }
50
51 void set_base_name(const irep_idt &base_name)
52 {
53 return set(ID_base_name, base_name);
54 }
55
56 void build(irept &src);
57};
58
60{
61 PRECONDITION(expr.id() == ID_declarator);
62 return static_cast<ansi_c_declaratort &>(expr);
63}
64
66{
67 PRECONDITION(expr.id() == ID_declarator);
68 return static_cast<const ansi_c_declaratort &>(expr);
69}
70
72{
73public:
77
78 bool get_is_typedef() const
79 {
80 return get_bool(ID_is_typedef);
81 }
82
83 void set_is_typedef(bool is_typedef)
84 {
85 set(ID_is_typedef, is_typedef);
86 }
87
89 {
91 }
92
97
98 bool get_is_static() const
99 {
100 return get_bool(ID_is_static);
101 }
102
103 void set_is_static(bool is_static)
104 {
105 set(ID_is_static, is_static);
106 }
107
108 bool get_is_parameter() const
109 {
111 }
112
113 void set_is_parameter(bool is_parameter)
114 {
115 set(ID_is_parameter, is_parameter);
116 }
117
118 bool get_is_member() const
119 {
120 return get_bool(ID_is_member);
121 }
122
123 void set_is_member(bool is_member)
124 {
125 set(ID_is_member, is_member);
126 }
127
128 bool get_is_global() const
129 {
130 return get_bool(ID_is_global);
131 }
132
134 {
136 }
137
138 bool get_is_register() const
139 {
140 return get_bool(ID_is_register);
141 }
142
143 void set_is_register(bool is_register)
144 {
145 set(ID_is_register, is_register);
146 }
147
149 {
151 }
152
153 void set_is_thread_local(bool is_thread_local)
154 {
155 set(ID_is_thread_local, is_thread_local);
156 }
157
158 bool get_is_inline() const
159 {
160 return get_bool(ID_is_inline);
161 }
162
163 void set_is_inline(bool is_inline)
164 {
165 set(ID_is_inline, is_inline);
166 }
167
168 bool get_is_extern() const
169 {
170 return get_bool(ID_is_extern);
171 }
172
173 void set_is_extern(bool is_extern)
174 {
175 set(ID_is_extern, is_extern);
176 }
177
179 {
181 }
182
183 void set_is_static_assert(bool is_static_assert)
184 {
185 set(ID_is_static_assert, is_static_assert);
186 }
187
188 bool get_is_weak() const
189 {
190 return get_bool(ID_is_weak);
191 }
192
193 void set_is_weak(bool is_weak)
194 {
195 set(ID_is_weak, is_weak);
196 }
197
198 symbolt to_symbol(const ansi_c_declaratort &) const;
199
200 typet full_type(const ansi_c_declaratort &) const;
201
202 typedef std::vector<ansi_c_declaratort> declaratorst;
203
205 {
206 return (const declaratorst &)operands();
207 }
208
210 {
211 return (declaratorst &)operands();
212 }
213
214 // special case of a declaration with exactly one declarator
216 {
217 PRECONDITION(declarators().size() == 1);
218 return declarators()[0];
219 }
220
222 {
223 PRECONDITION(declarators().size() == 1);
224 return declarators()[0];
225 }
226
227 void output(std::ostream &) const;
228
230 {
231 PRECONDITION(!declarators().empty());
232 declarators().back().value().swap(value);
233 }
234};
235
237{
238 PRECONDITION(expr.id() == ID_declaration);
239 return static_cast<ansi_c_declarationt &>(expr);
240}
241
243{
244 PRECONDITION(expr.id() == ID_declaration);
245 return static_cast<const ansi_c_declarationt &>(expr);
246}
247
248#endif // CPROVER_ANSI_C_ANSI_C_DECLARATION_H
ansi_c_declaratort & to_ansi_c_declarator(exprt &expr)
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void set_is_thread_local(bool is_thread_local)
void set_is_enum_constant(bool is_enum_constant)
const ansi_c_declaratort & declarator() const
void set_is_weak(bool is_weak)
symbolt to_symbol(const ansi_c_declaratort &) const
void set_is_parameter(bool is_parameter)
const declaratorst & declarators() const
void add_initializer(exprt &value)
std::vector< ansi_c_declaratort > declaratorst
void set_is_static_assert(bool is_static_assert)
void set_is_register(bool is_register)
declaratorst & declarators()
void set_is_inline(bool is_inline)
typet full_type(const ansi_c_declaratort &) const
bool get_is_enum_constant() const
void set_is_member(bool is_member)
ansi_c_declaratort & declarator()
void set_is_global(bool is_global)
void set_is_extern(bool is_extern)
bool get_is_thread_local() const
void set_is_typedef(bool is_typedef)
bool get_is_static_assert() const
void output(std::ostream &) const
void set_is_static(bool is_static)
void set_base_name(const irep_idt &base_name)
void set_name(const irep_idt &name)
irep_idt get_base_name() const
const exprt & value() const
irep_idt get_name() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
An expression without operands.
Definition std_expr.h:22
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.