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