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 
17 class symbolt;
18 
20 {
21 public:
22  ansi_c_declaratort() : nullary_exprt(ID_declarator, typet())
23  {
24  }
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  assert(expr.id()==ID_declarator);
62  return static_cast<ansi_c_declaratort &>(expr);
63 }
64 
65 inline const ansi_c_declaratort &to_ansi_c_declarator(const exprt &expr)
66 {
67  assert(expr.id()==ID_declarator);
68  return static_cast<const ansi_c_declaratort &>(expr);
69 }
70 
72 {
73 public:
74  ansi_c_declarationt():exprt(ID_declaration)
75  {
76  }
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 
88  bool get_is_enum_constant() const
89  {
90  return get_bool(ID_is_enum_constant);
91  }
92 
93  void set_is_enum_constant(bool is_enum_constant)
94  {
95  set(ID_is_enum_constant, is_enum_constant);
96  }
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  {
110  return get_bool(ID_is_parameter);
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 
133  void set_is_global(bool is_global)
134  {
135  set(ID_is_global, is_global);
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 
148  bool get_is_thread_local() const
149  {
150  return get_bool(ID_is_thread_local);
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 
178  bool get_is_static_assert() const
179  {
180  return get_bool(ID_is_static_assert);
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  bool get_is_used() const
199  {
200  return get_bool(ID_is_used);
201  }
202 
203  void set_is_used(bool is_used)
204  {
205  set(ID_is_used, is_used);
206  }
207 
208  void to_symbol(
209  const ansi_c_declaratort &,
210  symbolt &symbol) const;
211 
212  typet full_type(const ansi_c_declaratort &) const;
213 
214  typedef std::vector<ansi_c_declaratort> declaratorst;
215 
216  const declaratorst &declarators() const
217  {
218  return (const declaratorst &)operands();
219  }
220 
222  {
223  return (declaratorst &)operands();
224  }
225 
226  // special case of a declaration with exactly one declarator
228  {
229  assert(declarators().size()==1);
230  return declarators()[0];
231  }
232 
234  {
235  assert(declarators().size()==1);
236  return declarators()[0];
237  }
238 
239  void output(std::ostream &) const;
240 
241  void add_initializer(exprt &value)
242  {
243  assert(!declarators().empty());
244  declarators().back().value().swap(value);
245  }
246 
247  const exprt &spec_assigns() const
248  {
249  return static_cast<const exprt &>(find(ID_C_spec_assigns));
250  }
251 
252  const exprt &spec_requires() const
253  {
254  return static_cast<const exprt &>(find(ID_C_spec_requires));
255  }
256 
257  const exprt &spec_ensures() const
258  {
259  return static_cast<const exprt &>(find(ID_C_spec_ensures));
260  }
261 };
262 
264 {
265  assert(expr.id()==ID_declaration);
266  return static_cast<ansi_c_declarationt &>(expr);
267 }
268 
270 {
271  assert(expr.id()==ID_declaration);
272  return static_cast<const ansi_c_declarationt &>(expr);
273 }
274 
275 #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:92
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:116
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:58
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
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:28
API to expression classes.