cprover
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 "pointer_expr.h"
14 
19 {
20 public:
21  explicit c_bit_field_typet(typet _subtype, std::size_t width)
22  : bitvector_typet(ID_c_bit_field, width)
23  {
24  subtype().swap(_subtype);
25  }
26 
27  // These have a sub-type
28 };
29 
33 template <>
34 inline bool can_cast_type<c_bit_field_typet>(const typet &type)
35 {
36  return type.id() == ID_c_bit_field;
37 }
38 
47 inline const c_bit_field_typet &to_c_bit_field_type(const typet &type)
48 {
50  return static_cast<const c_bit_field_typet &>(type);
51 }
52 
55 {
57  return static_cast<c_bit_field_typet &>(type);
58 }
59 
62 {
63 public:
64  explicit c_bool_typet(std::size_t width) : bitvector_typet(ID_c_bool, width)
65  {
66  }
67 
68  static void check(
69  const typet &type,
71  {
72  DATA_CHECK(vm, !type.get(ID_width).empty(), "C bool type must have width");
73  }
74 };
75 
79 template <>
80 inline bool can_cast_type<c_bool_typet>(const typet &type)
81 {
82  return type.id() == ID_c_bool;
83 }
84 
93 inline const c_bool_typet &to_c_bool_type(const typet &type)
94 {
96  c_bool_typet::check(type);
97  return static_cast<const c_bool_typet &>(type);
98 }
99 
102 {
104  c_bool_typet::check(type);
105  return static_cast<c_bool_typet &>(type);
106 }
107 
112 {
113 public:
115  {
116  }
117 
118  explicit union_typet(componentst _components)
119  : struct_union_typet(ID_union, std::move(_components))
120  {
121  }
122 
129  find_widest_union_component(const namespacet &ns) const;
130 };
131 
135 template <>
136 inline bool can_cast_type<union_typet>(const typet &type)
137 {
138  return type.id() == ID_union;
139 }
140 
149 inline const union_typet &to_union_type(const typet &type)
150 {
152  return static_cast<const union_typet &>(type);
153 }
154 
157 {
159  return static_cast<union_typet &>(type);
160 }
161 
164 {
165 public:
166  explicit union_tag_typet(const irep_idt &identifier)
167  : tag_typet(ID_union_tag, identifier)
168  {
169  }
170 };
171 
175 template <>
176 inline bool can_cast_type<union_tag_typet>(const typet &type)
177 {
178  return type.id() == ID_union_tag;
179 }
180 
189 inline const union_tag_typet &to_union_tag_type(const typet &type)
190 {
192  return static_cast<const union_tag_typet &>(type);
193 }
194 
197 {
199  return static_cast<union_tag_typet &>(type);
200 }
201 
204 {
205 public:
206  explicit c_enum_typet(typet _subtype)
207  : type_with_subtypet(ID_c_enum, std::move(_subtype))
208  {
209  }
210 
211  class c_enum_membert : public irept
212  {
213  public:
215  {
216  return get(ID_value);
217  }
218  void set_value(const irep_idt &value)
219  {
220  set(ID_value, value);
221  }
223  {
224  return get(ID_identifier);
225  }
226  void set_identifier(const irep_idt &identifier)
227  {
228  set(ID_identifier, identifier);
229  }
231  {
232  return get(ID_base_name);
233  }
234  void set_base_name(const irep_idt &base_name)
235  {
236  set(ID_base_name, base_name);
237  }
238  };
239 
240  typedef std::vector<c_enum_membert> memberst;
241 
242  const memberst &members() const
243  {
244  return (const memberst &)(find(ID_body).get_sub());
245  }
246 
248  bool is_incomplete() const
249  {
250  return get_bool(ID_incomplete);
251  }
252 
255  {
256  set(ID_incomplete, true);
257  }
258 };
259 
263 template <>
264 inline bool can_cast_type<c_enum_typet>(const typet &type)
265 {
266  return type.id() == ID_c_enum;
267 }
268 
277 inline const c_enum_typet &to_c_enum_type(const typet &type)
278 {
280  return static_cast<const c_enum_typet &>(type);
281 }
282 
285 {
287  return static_cast<c_enum_typet &>(type);
288 }
289 
292 {
293 public:
294  explicit c_enum_tag_typet(const irep_idt &identifier)
295  : tag_typet(ID_c_enum_tag, identifier)
296  {
297  }
298 };
299 
303 template <>
304 inline bool can_cast_type<c_enum_tag_typet>(const typet &type)
305 {
306  return type.id() == ID_c_enum_tag;
307 }
308 
317 inline const c_enum_tag_typet &to_c_enum_tag_type(const typet &type)
318 {
320  return static_cast<const c_enum_tag_typet &>(type);
321 }
322 
325 {
327  return static_cast<c_enum_tag_typet &>(type);
328 }
329 
331 {
332 public:
337  code_with_contract_typet(parameterst _parameters, typet _return_type)
338  : code_typet(std::move(_parameters), std::move(_return_type))
339  {
340  }
341 
342  bool has_contract() const
343  {
344  return assigns().is_not_nil() || !requires().empty() || !ensures().empty();
345  }
346 
347  const exprt &assigns() const
348  {
349  return static_cast<const exprt &>(find(ID_C_spec_assigns));
350  }
351 
353  {
354  auto &result = static_cast<exprt &>(add(ID_C_spec_assigns));
355  if(result.id().empty()) // not initialized?
356  result.make_nil();
357  return result;
358  }
359 
360  const exprt::operandst &requires() const
361  {
362  return static_cast<const exprt &>(find(ID_C_spec_requires)).operands();
363  }
364 
366  {
367  return static_cast<exprt &>(add(ID_C_spec_requires)).operands();
368  }
369 
370  const exprt::operandst &ensures() const
371  {
372  return static_cast<const exprt &>(find(ID_C_spec_ensures)).operands();
373  }
374 
376  {
377  return static_cast<exprt &>(add(ID_C_spec_ensures)).operands();
378  }
379 };
380 
384 template <>
386 {
387  return type.id() == ID_code;
388 }
389 
398 inline const code_with_contract_typet &
400 {
403  return static_cast<const code_with_contract_typet &>(type);
404 }
405 
408 {
411  return static_cast<code_with_contract_typet &>(type);
412 }
413 
439 
440 // This is for Java and C++
442 
443 // Turns an ID_C_c_type into a string, e.g.,
444 // ID_signed_int gets "signed int".
445 std::string c_type_as_string(const irep_idt &);
446 
447 #endif // CPROVER_UTIL_C_TYPES_H
floatbv_typet float_type()
Definition: c_types.cpp:185
bitvector_typet index_type()
Definition: c_types.cpp:16
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
signedbv_typet signed_char_type()
Definition: c_types.cpp:142
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:34
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
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:80
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:175
bool can_cast_type< union_typet >(const typet &type)
Check whether a reference to a typet is a union_typet.
Definition: c_types.h:136
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
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:304
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
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:264
unsignedbv_typet size_type()
Definition: c_types.cpp:58
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
empty_typet void_type()
Definition: c_types.cpp:253
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:47
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
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:399
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
bitvector_typet char_type()
Definition: c_types.cpp:114
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
pointer_typet pointer_type(const typet &)
Definition: c_types.cpp:243
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:317
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
floatbv_typet long_double_type()
Definition: c_types.cpp:201
bitvector_typet enum_constant_type()
return type of enum constants
Definition: c_types.cpp:23
typet c_bool_type()
Definition: c_types.cpp:108
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:176
reference_typet reference_type(const typet &)
Definition: c_types.cpp:248
floatbv_typet double_type()
Definition: c_types.cpp:193
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:385
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:37
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:51
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:93
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:165
std::string c_type_as_string(const irep_idt &)
Definition: c_types.cpp:259
Base class of fixed-width bit-vector types.
Definition: std_types.h:832
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: c_types.h:19
c_bit_field_typet(typet _subtype, std::size_t width)
Definition: c_types.h:21
The C/C++ Booleans.
Definition: c_types.h:62
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: c_types.h:68
c_bool_typet(std::size_t width)
Definition: c_types.h:64
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:292
c_enum_tag_typet(const irep_idt &identifier)
Definition: c_types.h:294
void set_identifier(const irep_idt &identifier)
Definition: c_types.h:226
void set_value(const irep_idt &value)
Definition: c_types.h:218
irep_idt get_identifier() const
Definition: c_types.h:222
irep_idt get_base_name() const
Definition: c_types.h:230
void set_base_name(const irep_idt &base_name)
Definition: c_types.h:234
irep_idt get_value() const
Definition: c_types.h:214
The type of C enums.
Definition: c_types.h:204
const memberst & members() const
Definition: c_types.h:242
void make_incomplete()
enum types may be incomplete
Definition: c_types.h:254
std::vector< c_enum_membert > memberst
Definition: c_types.h:240
c_enum_typet(typet _subtype)
Definition: c_types.h:206
bool is_incomplete() const
enum types may be incomplete
Definition: c_types.h:248
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const exprt::operandst & requires() const
Definition: c_types.h:360
exprt::operandst & requires()
Definition: c_types.h:365
exprt::operandst & ensures()
Definition: c_types.h:375
const exprt & assigns() const
Definition: c_types.h:347
const exprt::operandst & ensures() const
Definition: c_types.h:370
bool has_contract() const
Definition: c_types.h:342
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:337
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
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:383
subt & get_sub()
Definition: irep.h:467
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
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
void swap(irept &irep)
Definition: irep.h:453
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
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:89
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:146
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
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:100
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:164
union_tag_typet(const irep_idt &identifier)
Definition: c_types.h:166
The union type.
Definition: c_types.h:112
union_typet()
Definition: c_types.h:114
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:308
union_typet(componentst _components)
Definition: c_types.h:118
Fixed-width bit-vector with unsigned binary interpretation.
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