CBMC
c_types.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_C_TYPES_H
11 #define CPROVER_UTIL_C_TYPES_H
12 
13 #include "deprecate.h"
14 #include "pointer_expr.h"
15 
20 {
21 public:
22  explicit c_bit_field_typet(typet _subtype, std::size_t width)
23  : bitvector_typet(ID_c_bit_field, width)
24  {
25  add_subtype() = std::move(_subtype);
26  }
27 
28  // These have a sub-type. The preferred way to access it
29  // are the underlying_type methods.
30  const typet &underlying_type() const
31  {
32  return subtype();
33  }
34 
36  {
37  return subtype();
38  }
39 
40  // Use .underlying_type() instead -- this method will be removed
41  const typet &subtype() const
42  {
43  // The existence of get_sub() front is enforced by check(...)
44  return static_cast<const typet &>(get_sub().front());
45  }
46 
47  // Use .underlying_type() instead -- this method will be removed
49  {
50  // The existence of get_sub() front is enforced by check(...)
51  return static_cast<typet &>(get_sub().front());
52  }
53 
54  static void check(
55  const typet &type,
57  {
58  bitvector_typet::check(type, vm);
59  type_with_subtypet::check(type, vm);
60  }
61 };
62 
66 template <>
67 inline bool can_cast_type<c_bit_field_typet>(const typet &type)
68 {
69  return type.id() == ID_c_bit_field;
70 }
71 
80 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
81 {
84  return static_cast<const c_bit_field_typet &>(type);
85 }
86 
89 {
92  return static_cast<c_bit_field_typet &>(type);
93 }
94 
97 {
98 public:
99  explicit c_bool_typet(std::size_t width) : bitvector_typet(ID_c_bool, width)
100  {
101  }
102 
103  static void check(
104  const typet &type,
106  {
107  DATA_CHECK(vm, !type.get(ID_width).empty(), "C bool type must have width");
108  }
109 };
110 
114 template <>
115 inline bool can_cast_type<c_bool_typet>(const typet &type)
116 {
117  return type.id() == ID_c_bool;
118 }
119 
128 inline const c_bool_typet &to_c_bool_type(const typet &type)
129 {
131  c_bool_typet::check(type);
132  return static_cast<const c_bool_typet &>(type);
133 }
134 
137 {
139  c_bool_typet::check(type);
140  return static_cast<c_bool_typet &>(type);
141 }
142 
147 {
148 public:
150  {
151  }
152 
153  explicit union_typet(componentst _components)
154  : struct_union_typet(ID_union, std::move(_components))
155  {
156  }
157 
163  std::optional<std::pair<struct_union_typet::componentt, mp_integer>>
164  find_widest_union_component(const namespacet &ns) const;
165 };
166 
170 template <>
171 inline bool can_cast_type<union_typet>(const typet &type)
172 {
173  return type.id() == ID_union;
174 }
175 
184 inline const union_typet &to_union_type(const typet &type)
185 {
187  return static_cast<const union_typet &>(type);
188 }
189 
192 {
194  return static_cast<union_typet &>(type);
195 }
196 
199 {
200 public:
201  explicit union_tag_typet(const irep_idt &identifier)
202  : struct_or_union_tag_typet(ID_union_tag, identifier)
203  {
204  }
205 };
206 
210 template <>
211 inline bool can_cast_type<union_tag_typet>(const typet &type)
212 {
213  return type.id() == ID_union_tag;
214 }
215 
224 inline const union_tag_typet &to_union_tag_type(const typet &type)
225 {
227  return static_cast<const union_tag_typet &>(type);
228 }
229 
232 {
234  return static_cast<union_tag_typet &>(type);
235 }
236 
239 {
240 public:
241  explicit c_enum_typet(typet _subtype)
242  : type_with_subtypet(ID_c_enum, std::move(_subtype))
243  {
244  }
245 
246  class c_enum_membert : public irept
247  {
248  public:
250  {
251  return get(ID_value);
252  }
253  void set_value(const irep_idt &value)
254  {
255  set(ID_value, value);
256  }
258  {
259  return get(ID_identifier);
260  }
261  void set_identifier(const irep_idt &identifier)
262  {
263  set(ID_identifier, identifier);
264  }
266  {
267  return get(ID_base_name);
268  }
269  void set_base_name(const irep_idt &base_name)
270  {
271  set(ID_base_name, base_name);
272  }
273  };
274 
275  typedef std::vector<c_enum_membert> memberst;
276 
277  c_enum_typet(typet _subtype, memberst enum_members)
278  : c_enum_typet(std::move(_subtype))
279  {
280  members() = std::move(enum_members);
281  }
282 
284  {
285  return reinterpret_cast<memberst &>(add(ID_body).get_sub());
286  }
287 
288  const memberst &members() const
289  {
290  return (const memberst &)(find(ID_body).get_sub());
291  }
292 
294  bool is_incomplete() const
295  {
296  return get_bool(ID_incomplete);
297  }
298 
301  {
302  set(ID_incomplete, true);
303  }
304 
305  // The preferred way to access the subtype
306  // are the underlying_type methods.
307  const typet &underlying_type() const
308  {
309  return subtype();
310  }
311 
313  {
314  return subtype();
315  }
316 };
317 
321 template <>
322 inline bool can_cast_type<c_enum_typet>(const typet &type)
323 {
324  return type.id() == ID_c_enum;
325 }
326 
335 inline const c_enum_typet &to_c_enum_type(const typet &type)
336 {
339  return static_cast<const c_enum_typet &>(type);
340 }
341 
344 {
347  return static_cast<c_enum_typet &>(type);
348 }
349 
352 {
353 public:
354  explicit c_enum_tag_typet(const irep_idt &identifier)
355  : tag_typet(ID_c_enum_tag, identifier)
356  {
357  }
358 };
359 
363 template <>
364 inline bool can_cast_type<c_enum_tag_typet>(const typet &type)
365 {
366  return type.id() == ID_c_enum_tag;
367 }
368 
377 inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
378 {
380  return static_cast<const c_enum_tag_typet &>(type);
381 }
382 
385 {
387  return static_cast<c_enum_tag_typet &>(type);
388 }
389 
391 {
392 public:
397  code_with_contract_typet(parameterst _parameters, typet _return_type)
398  : code_typet(std::move(_parameters), std::move(_return_type))
399  {
400  }
401 
402  bool has_contract() const
403  {
404  return !c_ensures().empty() || !c_requires().empty() ||
405  !c_assigns().empty() || !c_frees().empty();
406  }
407 
409  {
410  return static_cast<const exprt &>(find(ID_C_spec_assigns)).operands();
411  }
412 
414  {
415  return static_cast<exprt &>(add(ID_C_spec_assigns)).operands();
416  }
417 
418  const exprt::operandst &c_frees() const
419  {
420  return static_cast<const exprt &>(find(ID_C_spec_frees)).operands();
421  }
422 
424  {
425  return static_cast<exprt &>(add(ID_C_spec_frees)).operands();
426  }
427 
429  {
430  return static_cast<const exprt &>(find(ID_C_spec_requires)).operands();
431  }
432 
434  {
435  return static_cast<exprt &>(add(ID_C_spec_requires)).operands();
436  }
437 
439  {
440  return static_cast<const exprt &>(find(ID_C_spec_ensures)).operands();
441  }
442 
444  {
445  return static_cast<exprt &>(add(ID_C_spec_ensures)).operands();
446  }
447 };
448 
452 template <>
454 {
455  return type.id() == ID_code;
456 }
457 
466 inline const code_with_contract_typet &
468 {
471  return static_cast<const code_with_contract_typet &>(type);
472 }
473 
476 {
479  return static_cast<code_with_contract_typet &>(type);
480 }
481 
506 
507 // This is for Java and C++
509 
510 // Turns an ID_C_c_type into a string, e.g.,
511 // ID_signed_int gets "signed int".
512 std::string c_type_as_string(const irep_idt &);
513 
514 #endif // CPROVER_UTIL_C_TYPES_H
floatbv_typet float_type()
Definition: c_types.cpp:177
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:72
signedbv_typet signed_char_type()
Definition: c_types.cpp:134
bool can_cast_type< c_bit_field_typet >(const typet &type)
Check whether a reference to a typet is a c_bit_field_typet.
Definition: c_types.h:67
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:36
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:93
bool can_cast_type< c_bool_typet >(const typet &type)
Check whether a reference to a typet is a c_bool_typet.
Definition: c_types.h:115
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:167
bool can_cast_type< union_typet >(const typet &type)
Check whether a reference to a typet is a union_typet.
Definition: c_types.h:171
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:86
bool can_cast_type< c_enum_tag_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_tag_typet.
Definition: c_types.h:364
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:335
bool can_cast_type< c_enum_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_typet.
Definition: c_types.h:322
unsignedbv_typet size_type()
Definition: c_types.cpp:50
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
empty_typet void_type()
Definition: c_types.cpp:245
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:80
signedbv_typet signed_int_type()
Definition: c_types.cpp:22
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition: c_types.h:467
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:220
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:127
signedbv_typet signed_size_type()
Definition: c_types.cpp:66
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:184
bitvector_typet char_type()
Definition: c_types.cpp:106
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:79
pointer_typet pointer_type(const typet &)
Definition: c_types.cpp:235
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:377
bitvector_typet wchar_t_type()
Definition: c_types.cpp:141
floatbv_typet long_double_type()
Definition: c_types.cpp:193
typet c_bool_type()
Definition: c_types.cpp:100
bool can_cast_type< union_tag_typet >(const typet &type)
Check whether a reference to a typet is a union_tag_typet.
Definition: c_types.h:211
bitvector_typet c_index_type()
Definition: c_types.cpp:16
reference_typet reference_type(const typet &)
Definition: c_types.cpp:240
floatbv_typet double_type()
Definition: c_types.cpp:185
bool can_cast_type< code_with_contract_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: c_types.h:453
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:29
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:43
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:128
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:157
std::string c_type_as_string(const irep_idt &)
Definition: c_types.cpp:251
Base class of fixed-width bit-vector types.
Definition: std_types.h:909
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_types.h:930
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: c_types.h:20
c_bit_field_typet(typet _subtype, std::size_t width)
Definition: c_types.h:22
typet & underlying_type()
Definition: c_types.h:35
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: c_types.h:54
const typet & subtype() const
Definition: c_types.h:41
typet & subtype()
Definition: c_types.h:48
const typet & underlying_type() const
Definition: c_types.h:30
The C/C++ Booleans.
Definition: c_types.h:97
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: c_types.h:103
c_bool_typet(std::size_t width)
Definition: c_types.h:99
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:352
c_enum_tag_typet(const irep_idt &identifier)
Definition: c_types.h:354
void set_identifier(const irep_idt &identifier)
Definition: c_types.h:261
void set_value(const irep_idt &value)
Definition: c_types.h:253
irep_idt get_identifier() const
Definition: c_types.h:257
irep_idt get_base_name() const
Definition: c_types.h:265
void set_base_name(const irep_idt &base_name)
Definition: c_types.h:269
irep_idt get_value() const
Definition: c_types.h:249
The type of C enums.
Definition: c_types.h:239
c_enum_typet(typet _subtype, memberst enum_members)
Definition: c_types.h:277
typet & underlying_type()
Definition: c_types.h:312
memberst & members()
Definition: c_types.h:283
const memberst & members() const
Definition: c_types.h:288
void make_incomplete()
enum types may be incomplete
Definition: c_types.h:300
const typet & underlying_type() const
Definition: c_types.h:307
std::vector< c_enum_membert > memberst
Definition: c_types.h:275
c_enum_typet(typet _subtype)
Definition: c_types.h:241
bool is_incomplete() const
enum types may be incomplete
Definition: c_types.h:294
Base type of functions.
Definition: std_types.h:583
std::vector< parametert > parameterst
Definition: std_types.h:585
const exprt::operandst & c_assigns() const
Definition: c_types.h:408
const exprt::operandst & c_requires() const
Definition: c_types.h:428
exprt::operandst & c_assigns()
Definition: c_types.h:413
const exprt::operandst & c_frees() const
Definition: c_types.h:418
exprt::operandst & c_ensures()
Definition: c_types.h:443
exprt::operandst & c_frees()
Definition: c_types.h:423
exprt::operandst & c_requires()
Definition: c_types.h:433
const exprt::operandst & c_ensures() const
Definition: c_types.h:438
bool has_contract() const
Definition: c_types.h:402
code_with_contract_typet(parameterst _parameters, typet _return_type)
Constructs a new 'code with contract' type, i.e., a function type decorated with a function contract.
Definition: c_types.h:397
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
Fixed-width bit-vector with IEEE floating-point interpretation.
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
subt & get_sub()
Definition: irep.h:444
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The reference type.
Definition: pointer_expr.h:121
Fixed-width bit-vector with two's complement interpretation.
A struct or union tag type.
Definition: std_types.h:451
Base type for structs and unions.
Definition: std_types.h:62
std::vector< componentt > componentst
Definition: std_types.h:140
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:396
Type with a single subtype.
Definition: type.h:180
const typet & subtype() const
Definition: type.h:187
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:199
The type of an expression, extends irept.
Definition: type.h:29
typet & add_subtype()
Definition: type.h:53
static void check(const typet &, const validation_modet=validation_modet::INVARIANT)
Check that the type is well-formed (shallow checks only, i.e., subtypes are not checked)
Definition: type.h:134
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:199
union_tag_typet(const irep_idt &identifier)
Definition: c_types.h:201
The union type.
Definition: c_types.h:147
union_typet()
Definition: c_types.h:149
union_typet(componentst _components)
Definition: c_types.h:153
std::optional< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition: c_types.cpp:300
Fixed-width bit-vector with unsigned binary interpretation.
API to expression classes for Pointers.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet