CBMC
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  PRECONDITION(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  PRECONDITION(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  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 
204  const declaratorst &declarators() const
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 
229  void add_initializer(exprt &value)
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)
void set_is_thread_local(bool is_thread_local)
void set_is_enum_constant(bool is_enum_constant)
void set_is_weak(bool is_weak)
symbolt to_symbol(const ansi_c_declaratort &) const
void set_is_parameter(bool is_parameter)
bool get_is_parameter() 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)
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
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
bool get_is_typedef() const
ansi_c_declaratort & declarator()
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)
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: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:360
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:408
const irep_idt & id() const
Definition: irep.h:384
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.