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  subtype().swap(_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 
44 template <>
45 inline bool can_cast_type<c_bit_field_typet>(const typet &type)
46 {
47  return type.id() == ID_c_bit_field;
48 }
49 
58 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
59 {
62  return static_cast<const c_bit_field_typet &>(type);
63 }
64 
67 {
70  return static_cast<c_bit_field_typet &>(type);
71 }
72 
75 {
76 public:
77  explicit c_bool_typet(std::size_t width) : bitvector_typet(ID_c_bool, width)
78  {
79  }
80 
81  static void check(
82  const typet &type,
84  {
85  DATA_CHECK(vm, !type.get(ID_width).empty(), "C bool type must have width");
86  }
87 };
88 
92 template <>
93 inline bool can_cast_type<c_bool_typet>(const typet &type)
94 {
95  return type.id() == ID_c_bool;
96 }
97 
106 inline const c_bool_typet &to_c_bool_type(const typet &type)
107 {
109  c_bool_typet::check(type);
110  return static_cast<const c_bool_typet &>(type);
111 }
112 
115 {
117  c_bool_typet::check(type);
118  return static_cast<c_bool_typet &>(type);
119 }
120 
125 {
126 public:
128  {
129  }
130 
131  explicit union_typet(componentst _components)
132  : struct_union_typet(ID_union, std::move(_components))
133  {
134  }
135 
142  find_widest_union_component(const namespacet &ns) const;
143 };
144 
148 template <>
149 inline bool can_cast_type<union_typet>(const typet &type)
150 {
151  return type.id() == ID_union;
152 }
153 
162 inline const union_typet &to_union_type(const typet &type)
163 {
165  return static_cast<const union_typet &>(type);
166 }
167 
170 {
172  return static_cast<union_typet &>(type);
173 }
174 
177 {
178 public:
179  explicit union_tag_typet(const irep_idt &identifier)
180  : tag_typet(ID_union_tag, identifier)
181  {
182  }
183 };
184 
188 template <>
189 inline bool can_cast_type<union_tag_typet>(const typet &type)
190 {
191  return type.id() == ID_union_tag;
192 }
193 
202 inline const union_tag_typet &to_union_tag_type(const typet &type)
203 {
205  return static_cast<const union_tag_typet &>(type);
206 }
207 
210 {
212  return static_cast<union_tag_typet &>(type);
213 }
214 
217 {
218 public:
219  explicit c_enum_typet(typet _subtype)
220  : type_with_subtypet(ID_c_enum, std::move(_subtype))
221  {
222  }
223 
224  class c_enum_membert : public irept
225  {
226  public:
228  {
229  return get(ID_value);
230  }
231  void set_value(const irep_idt &value)
232  {
233  set(ID_value, value);
234  }
236  {
237  return get(ID_identifier);
238  }
239  void set_identifier(const irep_idt &identifier)
240  {
241  set(ID_identifier, identifier);
242  }
244  {
245  return get(ID_base_name);
246  }
247  void set_base_name(const irep_idt &base_name)
248  {
249  set(ID_base_name, base_name);
250  }
251  };
252 
253  typedef std::vector<c_enum_membert> memberst;
254 
255  const memberst &members() const
256  {
257  return (const memberst &)(find(ID_body).get_sub());
258  }
259 
261  bool is_incomplete() const
262  {
263  return get_bool(ID_incomplete);
264  }
265 
268  {
269  set(ID_incomplete, true);
270  }
271 
272  // The preferred way to access the subtype
273  // are the underlying_type methods.
274  const typet &underlying_type() const
275  {
276  return subtype();
277  }
278 
280  {
281  return subtype();
282  }
283 };
284 
288 template <>
289 inline bool can_cast_type<c_enum_typet>(const typet &type)
290 {
291  return type.id() == ID_c_enum;
292 }
293 
302 inline const c_enum_typet &to_c_enum_type(const typet &type)
303 {
306  return static_cast<const c_enum_typet &>(type);
307 }
308 
311 {
314  return static_cast<c_enum_typet &>(type);
315 }
316 
319 {
320 public:
321  explicit c_enum_tag_typet(const irep_idt &identifier)
322  : tag_typet(ID_c_enum_tag, identifier)
323  {
324  }
325 };
326 
330 template <>
331 inline bool can_cast_type<c_enum_tag_typet>(const typet &type)
332 {
333  return type.id() == ID_c_enum_tag;
334 }
335 
344 inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
345 {
347  return static_cast<const c_enum_tag_typet &>(type);
348 }
349 
352 {
354  return static_cast<c_enum_tag_typet &>(type);
355 }
356 
358 {
359 public:
364  code_with_contract_typet(parameterst _parameters, typet _return_type)
365  : code_typet(std::move(_parameters), std::move(_return_type))
366  {
367  }
368 
369  bool has_contract() const
370  {
371  return !ensures().empty() || !requires().empty() || !assigns().empty() ||
372  !frees().empty();
373  }
374 
375  const exprt::operandst &assigns() const
376  {
377  return static_cast<const exprt &>(find(ID_C_spec_assigns)).operands();
378  }
379 
381  {
382  return static_cast<exprt &>(add(ID_C_spec_assigns)).operands();
383  }
384 
385  const exprt::operandst &frees() const
386  {
387  return static_cast<const exprt &>(find(ID_C_spec_frees)).operands();
388  }
389 
391  {
392  return static_cast<exprt &>(add(ID_C_spec_frees)).operands();
393  }
394 
395  const exprt::operandst &requires() const
396  {
397  return static_cast<const exprt &>(find(ID_C_spec_requires)).operands();
398  }
399 
401  {
402  return static_cast<exprt &>(add(ID_C_spec_requires)).operands();
403  }
404 
405  const exprt::operandst &ensures() const
406  {
407  return static_cast<const exprt &>(find(ID_C_spec_ensures)).operands();
408  }
409 
411  {
412  return static_cast<exprt &>(add(ID_C_spec_ensures)).operands();
413  }
414 };
415 
419 template <>
421 {
422  return type.id() == ID_code;
423 }
424 
433 inline const code_with_contract_typet &
435 {
438  return static_cast<const code_with_contract_typet &>(type);
439 }
440 
443 {
446  return static_cast<code_with_contract_typet &>(type);
447 }
448 
449 DEPRECATED(
450  SINCE(2022, 1, 13, "use c_index_type() or array_typet::index_type() instead"))
452 
477 
478 // This is for Java and C++
480 
481 // Turns an ID_C_c_type into a string, e.g.,
482 // ID_signed_int gets "signed int".
483 std::string c_type_as_string(const irep_idt &);
484 
485 #endif // CPROVER_UTIL_C_TYPES_H
floatbv_typet float_type()
Definition: c_types.cpp:182
bitvector_typet index_type()
Definition: c_types.cpp:22
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:77
signedbv_typet signed_char_type()
Definition: c_types.cpp:139
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:45
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:41
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:98
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:93
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:172
bool can_cast_type< union_typet >(const typet &type)
Check whether a reference to a typet is a union_typet.
Definition: c_types.h:149
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:91
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:331
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
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:289
unsignedbv_typet size_type()
Definition: c_types.cpp:55
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
empty_typet void_type()
Definition: c_types.cpp:250
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:58
signedbv_typet signed_int_type()
Definition: c_types.cpp:27
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:434
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:225
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:132
signedbv_typet signed_size_type()
Definition: c_types.cpp:71
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
bitvector_typet char_type()
Definition: c_types.cpp:111
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:84
pointer_typet pointer_type(const typet &)
Definition: c_types.cpp:240
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:344
bitvector_typet wchar_t_type()
Definition: c_types.cpp:146
floatbv_typet long_double_type()
Definition: c_types.cpp:198
typet c_bool_type()
Definition: c_types.cpp:105
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:189
bitvector_typet c_index_type()
Definition: c_types.cpp:16
reference_typet reference_type(const typet &)
Definition: c_types.cpp:245
floatbv_typet double_type()
Definition: c_types.cpp:190
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:420
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:34
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:48
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:106
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:162
std::string c_type_as_string(const irep_idt &)
Definition: c_types.cpp:256
Base class of fixed-width bit-vector types.
Definition: std_types.h:865
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
const typet & underlying_type() const
Definition: c_types.h:30
The C/C++ Booleans.
Definition: c_types.h:75
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: c_types.h:81
c_bool_typet(std::size_t width)
Definition: c_types.h:77
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:319
c_enum_tag_typet(const irep_idt &identifier)
Definition: c_types.h:321
void set_identifier(const irep_idt &identifier)
Definition: c_types.h:239
void set_value(const irep_idt &value)
Definition: c_types.h:231
irep_idt get_identifier() const
Definition: c_types.h:235
irep_idt get_base_name() const
Definition: c_types.h:243
void set_base_name(const irep_idt &base_name)
Definition: c_types.h:247
irep_idt get_value() const
Definition: c_types.h:227
The type of C enums.
Definition: c_types.h:217
typet & underlying_type()
Definition: c_types.h:279
const memberst & members() const
Definition: c_types.h:255
void make_incomplete()
enum types may be incomplete
Definition: c_types.h:267
const typet & underlying_type() const
Definition: c_types.h:274
std::vector< c_enum_membert > memberst
Definition: c_types.h:253
c_enum_typet(typet _subtype)
Definition: c_types.h:219
bool is_incomplete() const
enum types may be incomplete
Definition: c_types.h:261
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
exprt::operandst & assigns()
Definition: c_types.h:380
const exprt::operandst & requires() const
Definition: c_types.h:395
exprt::operandst & frees()
Definition: c_types.h:390
exprt::operandst & requires()
Definition: c_types.h:400
const exprt::operandst & assigns() const
Definition: c_types.h:375
const exprt::operandst & frees() const
Definition: c_types.h:385
exprt::operandst & ensures()
Definition: c_types.h:410
const exprt::operandst & ensures() const
Definition: c_types.h:405
bool has_contract() const
Definition: c_types.h:369
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:364
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:39
bool empty() const
Definition: dstring.h:90
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:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:456
const irept & find(const irep_idt &name) const
Definition: irep.cpp:105
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:420
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
irept & add(const irep_idt &name)
Definition: irep.cpp:115
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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:107
Fixed-width bit-vector with two's complement interpretation.
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:165
const typet & subtype() const
Definition: type.h:172
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:184
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:50
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:119
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:177
union_tag_typet(const irep_idt &identifier)
Definition: c_types.h:179
The union type.
Definition: c_types.h:125
union_typet()
Definition: c_types.h:127
optionalt< 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:305
union_typet(componentst _components)
Definition: c_types.h:131
Fixed-width bit-vector with unsigned binary interpretation.
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
#define DEPRECATED(msg)
Definition: deprecate.h:23
nonstd::optional< T > optionalt
Definition: optional.h:35
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