cprover
ansi_c_declaration.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-CC Language Type Checking
4 
5 Author: 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 <cassert>
16 
17 #include <util/std_expr.h>
18 #include <util/symbol.h>
19 
21 {
22 public:
23  ansi_c_declaratort() : nullary_exprt(ID_declarator, typet())
24  {
25  }
26 
28  {
29  return static_cast<exprt &>(add(ID_value));
30  }
31 
32  const exprt &value() const
33  {
34  return static_cast<const exprt &>(find(ID_value));
35  }
36 
37  void set_name(const irep_idt &name)
38  {
39  return set(ID_name, name);
40  }
41 
43  {
44  return get(ID_name);
45  }
46 
48  {
49  return get(ID_base_name);
50  }
51 
52  void set_base_name(const irep_idt &base_name)
53  {
54  return set(ID_base_name, base_name);
55  }
56 
57  void build(irept &src);
58 };
59 
61 {
62  assert(expr.id()==ID_declarator);
63  return static_cast<ansi_c_declaratort &>(expr);
64 }
65 
66 inline const ansi_c_declaratort &to_ansi_c_declarator(const exprt &expr)
67 {
68  assert(expr.id()==ID_declarator);
69  return static_cast<const ansi_c_declaratort &>(expr);
70 }
71 
73 {
74 public:
75  ansi_c_declarationt():exprt(ID_declaration)
76  {
77  }
78 
79  bool get_is_typedef() const
80  {
81  return get_bool(ID_is_typedef);
82  }
83 
84  void set_is_typedef(bool is_typedef)
85  {
86  set(ID_is_typedef, is_typedef);
87  }
88 
89  bool get_is_enum_constant() const
90  {
91  return get_bool(ID_is_enum_constant);
92  }
93 
94  void set_is_enum_constant(bool is_enum_constant)
95  {
96  set(ID_is_enum_constant, is_enum_constant);
97  }
98 
99  bool get_is_static() const
100  {
101  return get_bool(ID_is_static);
102  }
103 
104  void set_is_static(bool is_static)
105  {
106  set(ID_is_static, is_static);
107  }
108 
109  bool get_is_parameter() const
110  {
111  return get_bool(ID_is_parameter);
112  }
113 
114  void set_is_parameter(bool is_parameter)
115  {
116  set(ID_is_parameter, is_parameter);
117  }
118 
119  bool get_is_member() const
120  {
121  return get_bool(ID_is_member);
122  }
123 
124  void set_is_member(bool is_member)
125  {
126  set(ID_is_member, is_member);
127  }
128 
129  bool get_is_global() const
130  {
131  return get_bool(ID_is_global);
132  }
133 
134  void set_is_global(bool is_global)
135  {
136  set(ID_is_global, is_global);
137  }
138 
139  bool get_is_register() const
140  {
141  return get_bool(ID_is_register);
142  }
143 
144  void set_is_register(bool is_register)
145  {
146  set(ID_is_register, is_register);
147  }
148 
149  bool get_is_thread_local() const
150  {
151  return get_bool(ID_is_thread_local);
152  }
153 
154  void set_is_thread_local(bool is_thread_local)
155  {
156  set(ID_is_thread_local, is_thread_local);
157  }
158 
159  bool get_is_inline() const
160  {
161  return get_bool(ID_is_inline);
162  }
163 
164  void set_is_inline(bool is_inline)
165  {
166  set(ID_is_inline, is_inline);
167  }
168 
169  bool get_is_extern() const
170  {
171  return get_bool(ID_is_extern);
172  }
173 
174  void set_is_extern(bool is_extern)
175  {
176  set(ID_is_extern, is_extern);
177  }
178 
179  bool get_is_static_assert() const
180  {
181  return get_bool(ID_is_static_assert);
182  }
183 
184  void set_is_static_assert(bool is_static_assert)
185  {
186  set(ID_is_static_assert, is_static_assert);
187  }
188 
189  bool get_is_weak() const
190  {
191  return get_bool(ID_is_weak);
192  }
193 
194  void set_is_weak(bool is_weak)
195  {
196  set(ID_is_weak, is_weak);
197  }
198 
199  bool get_is_used() const
200  {
201  return get_bool(ID_is_used);
202  }
203 
204  void set_is_used(bool is_used)
205  {
206  set(ID_is_used, is_used);
207  }
208 
209  void to_symbol(
210  const ansi_c_declaratort &,
211  symbolt &symbol) const;
212 
213  typet full_type(const ansi_c_declaratort &) const;
214 
215  typedef std::vector<ansi_c_declaratort> declaratorst;
216 
217  const declaratorst &declarators() const
218  {
219  return (const declaratorst &)operands();
220  }
221 
223  {
224  return (declaratorst &)operands();
225  }
226 
227  // special case of a declaration with exactly one declarator
229  {
230  assert(declarators().size()==1);
231  return declarators()[0];
232  }
233 
235  {
236  assert(declarators().size()==1);
237  return declarators()[0];
238  }
239 
240  void output(std::ostream &) const;
241 
242  void add_initializer(exprt &value)
243  {
244  assert(!declarators().empty());
245  declarators().back().value().swap(value);
246  }
247 
248  const exprt &spec_assigns() const
249  {
250  return static_cast<const exprt &>(find(ID_C_spec_assigns));
251  }
252 
253  const exprt &spec_requires() const
254  {
255  return static_cast<const exprt &>(find(ID_C_spec_requires));
256  }
257 
258  const exprt &spec_ensures() const
259  {
260  return static_cast<const exprt &>(find(ID_C_spec_ensures));
261  }
262 };
263 
265 {
266  assert(expr.id()==ID_declaration);
267  return static_cast<ansi_c_declarationt &>(expr);
268 }
269 
271 {
272  assert(expr.id()==ID_declaration);
273  return static_cast<const ansi_c_declarationt &>(expr);
274 }
275 
276 #endif // CPROVER_ANSI_C_ANSI_C_DECLARATION_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ansi_c_declaratort::value
const exprt & value() const
Definition: ansi_c_declaration.h:32
ansi_c_declarationt::spec_requires
const exprt & spec_requires() const
Definition: ansi_c_declaration.h:253
ansi_c_declarationt::get_is_thread_local
bool get_is_thread_local() const
Definition: ansi_c_declaration.h:149
ansi_c_declarationt::declarators
const declaratorst & declarators() const
Definition: ansi_c_declaration.h:217
ansi_c_declarationt::set_is_parameter
void set_is_parameter(bool is_parameter)
Definition: ansi_c_declaration.h:114
ansi_c_declarationt::get_is_typedef
bool get_is_typedef() const
Definition: ansi_c_declaration.h:79
to_ansi_c_declarator
ansi_c_declaratort & to_ansi_c_declarator(exprt &expr)
Definition: ansi_c_declaration.h:60
ansi_c_declarationt::get_is_used
bool get_is_used() const
Definition: ansi_c_declaration.h:199
ansi_c_declaratort::value
exprt & value()
Definition: ansi_c_declaration.h:27
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
typet
The type of an expression, extends irept.
Definition: type.h:29
ansi_c_declarationt::get_is_static
bool get_is_static() const
Definition: ansi_c_declaration.h:99
ansi_c_declarationt::get_is_weak
bool get_is_weak() const
Definition: ansi_c_declaration.h:189
ansi_c_declarationt::add_initializer
void add_initializer(exprt &value)
Definition: ansi_c_declaration.h:242
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
ansi_c_declarationt::set_is_enum_constant
void set_is_enum_constant(bool is_enum_constant)
Definition: ansi_c_declaration.h:94
exprt
Base class for all expressions.
Definition: expr.h:53
ansi_c_declarationt::set_is_global
void set_is_global(bool is_global)
Definition: ansi_c_declaration.h:134
ansi_c_declarationt::declarator
const ansi_c_declaratort & declarator() const
Definition: ansi_c_declaration.h:228
ansi_c_declarationt::declarators
declaratorst & declarators()
Definition: ansi_c_declaration.h:222
ansi_c_declarationt::get_is_static_assert
bool get_is_static_assert() const
Definition: ansi_c_declaration.h:179
ansi_c_declaratort::set_base_name
void set_base_name(const irep_idt &base_name)
Definition: ansi_c_declaration.h:52
ansi_c_declarationt::set_is_typedef
void set_is_typedef(bool is_typedef)
Definition: ansi_c_declaration.h:84
ansi_c_declaratort::get_name
irep_idt get_name() const
Definition: ansi_c_declaration.h:42
ansi_c_declarationt::ansi_c_declarationt
ansi_c_declarationt()
Definition: ansi_c_declaration.h:75
ansi_c_declaratort::build
void build(irept &src)
Definition: ansi_c_declaration.cpp:23
nullary_exprt
An expression without operands.
Definition: std_expr.h:24
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
ansi_c_declarationt::get_is_parameter
bool get_is_parameter() const
Definition: ansi_c_declaration.h:109
ansi_c_declaratort
Definition: ansi_c_declaration.h:21
ansi_c_declarationt::set_is_register
void set_is_register(bool is_register)
Definition: ansi_c_declaration.h:144
ansi_c_declaratort::get_base_name
irep_idt get_base_name() const
Definition: ansi_c_declaration.h:47
ansi_c_declarationt::set_is_weak
void set_is_weak(bool is_weak)
Definition: ansi_c_declaration.h:194
ansi_c_declarationt::to_symbol
void to_symbol(const ansi_c_declaratort &, symbolt &symbol) const
Definition: ansi_c_declaration.cpp:126
ansi_c_declarationt::get_is_register
bool get_is_register() const
Definition: ansi_c_declaration.h:139
symbol.h
Symbol table entry.
ansi_c_declarationt::get_is_enum_constant
bool get_is_enum_constant() const
Definition: ansi_c_declaration.h:89
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_ansi_c_declaration
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
Definition: ansi_c_declaration.h:264
ansi_c_declarationt::spec_assigns
const exprt & spec_assigns() const
Definition: ansi_c_declaration.h:248
ansi_c_declarationt::get_is_member
bool get_is_member() const
Definition: ansi_c_declaration.h:119
ansi_c_declarationt::spec_ensures
const exprt & spec_ensures() const
Definition: ansi_c_declaration.h:258
ansi_c_declarationt::set_is_thread_local
void set_is_thread_local(bool is_thread_local)
Definition: ansi_c_declaration.h:154
ansi_c_declarationt
Definition: ansi_c_declaration.h:73
ansi_c_declaratort::set_name
void set_name(const irep_idt &name)
Definition: ansi_c_declaration.h:37
ansi_c_declarationt::set_is_static
void set_is_static(bool is_static)
Definition: ansi_c_declaration.h:104
ansi_c_declarationt::get_is_global
bool get_is_global() const
Definition: ansi_c_declaration.h:129
ansi_c_declarationt::get_is_extern
bool get_is_extern() const
Definition: ansi_c_declaration.h:169
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
ansi_c_declarationt::declarator
ansi_c_declaratort & declarator()
Definition: ansi_c_declaration.h:234
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
ansi_c_declarationt::set_is_static_assert
void set_is_static_assert(bool is_static_assert)
Definition: ansi_c_declaration.h:184
ansi_c_declarationt::set_is_extern
void set_is_extern(bool is_extern)
Definition: ansi_c_declaration.h:174
ansi_c_declarationt::output
void output(std::ostream &) const
Definition: ansi_c_declaration.cpp:63
ansi_c_declaratort::ansi_c_declaratort
ansi_c_declaratort()
Definition: ansi_c_declaration.h:23
ansi_c_declarationt::full_type
typet full_type(const ansi_c_declaratort &) const
Definition: ansi_c_declaration.cpp:94
ansi_c_declarationt::set_is_member
void set_is_member(bool is_member)
Definition: ansi_c_declaration.h:124
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
exprt::operands
operandst & operands()
Definition: expr.h:95
ansi_c_declarationt::declaratorst
std::vector< ansi_c_declaratort > declaratorst
Definition: ansi_c_declaration.h:215
std_expr.h
API to expression classes.
ansi_c_declarationt::set_is_inline
void set_is_inline(bool is_inline)
Definition: ansi_c_declaration.h:164
ansi_c_declarationt::set_is_used
void set_is_used(bool is_used)
Definition: ansi_c_declaration.h:204
ansi_c_declarationt::get_is_inline
bool get_is_inline() const
Definition: ansi_c_declaration.h:159