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
ansi_c_declaratort & to_ansi_c_declarator(exprt &expr)
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
void set_is_thread_local(bool is_thread_local)
const exprt & spec_assigns() const
void set_is_enum_constant(bool is_enum_constant)
void set_is_weak(bool is_weak)
void set_is_parameter(bool is_parameter)
bool get_is_parameter() const
void add_initializer(exprt &value)
const exprt & spec_requires() const
std::vector< ansi_c_declaratort > declaratorst
void set_is_static_assert(bool is_static_assert)
void set_is_register(bool is_register)
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)
bool get_is_static() const
const ansi_c_declaratort & declarator() const
void to_symbol(const ansi_c_declaratort &, symbolt &symbol) const
declaratorst & declarators()
void set_is_global(bool is_global)
const declaratorst & declarators() const
bool get_is_register() const
void set_is_extern(bool is_extern)
bool get_is_thread_local() const
void set_is_used(bool is_used)
bool get_is_typedef() const
ansi_c_declaratort & declarator()
void set_is_typedef(bool is_typedef)
bool get_is_static_assert() const
const exprt & spec_ensures() const
void output(std::ostream &) const
void set_is_static(bool is_static)
const exprt & value() const
void set_base_name(const irep_idt &base_name)
void set_name(const irep_idt &name)
void build(irept &src)
irep_idt get_base_name() 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:37
Base class for all expressions.
Definition: expr.h:54
operandst & operands()
Definition: expr.h:96
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
irept & add(const irep_namet &name)
Definition: irep.cpp:113
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
An expression without operands.
Definition: std_expr.h:23
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
API to expression classes.
Symbol table entry.