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
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
to_code_with_contract_type
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
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
typet::subtype
const typet & subtype() const
Definition: type.h:47
to_c_bool_type
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:93
c_enum_typet
The type of C enums.
Definition: c_types.h:204
c_enum_typet::c_enum_typet
c_enum_typet(typet _subtype)
Definition: c_types.h:206
c_enum_typet::c_enum_membert::set_value
void set_value(const irep_idt &value)
Definition: c_types.h:218
c_type_as_string
std::string c_type_as_string(const irep_idt &)
Definition: c_types.cpp:259
c_enum_typet::is_incomplete
bool is_incomplete() const
enum types may be incomplete
Definition: c_types.h:248
reference_typet
The reference type.
Definition: pointer_expr.h:89
irept::make_nil
void make_nil()
Definition: irep.h:465
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:541
c_bit_field_typet::c_bit_field_typet
c_bit_field_typet(typet _subtype, std::size_t width)
Definition: c_types.h:21
union_typet::find_widest_union_component
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
char32_t_type
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:175
c_bool_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: c_types.h:68
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:62
can_cast_type< union_tag_typet >
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
c_enum_typet::memberst
std::vector< c_enum_membert > memberst
Definition: c_types.h:240
can_cast_type< c_bool_typet >
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
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:116
double_type
floatbv_typet double_type()
Definition: c_types.cpp:193
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: bitvector_types.h:322
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:140
c_bool_type
typet c_bool_type()
Definition: c_types.cpp:108
c_enum_typet::make_incomplete
void make_incomplete()
enum types may be incomplete
Definition: c_types.h:254
code_with_contract_typet::assigns
const exprt & assigns() const
Definition: c_types.h:347
enum_constant_type
bitvector_typet enum_constant_type()
return type of enum constants
Definition: c_types.cpp:23
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
type_with_subtypet
Type with a single subtype.
Definition: type.h:146
c_enum_typet::c_enum_membert::get_base_name
irep_idt get_base_name() const
Definition: c_types.h:230
reference_type
reference_typet reference_type(const typet &)
Definition: c_types.cpp:248
union_tag_typet
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:164
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
union_typet::union_typet
union_typet(componentst _components)
Definition: c_types.h:118
unsigned_long_int_type
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
c_bool_typet
The C/C++ Booleans.
Definition: c_types.h:62
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
empty_typet
The empty type.
Definition: std_types.h:51
c_bit_field_typet
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: c_types.h:19
can_cast_type< c_enum_tag_typet >
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
can_cast_type< code_with_contract_typet >
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
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
to_c_enum_tag_type
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
signed_char_type
signedbv_typet signed_char_type()
Definition: c_types.cpp:142
long_double_type
floatbv_typet long_double_type()
Definition: c_types.cpp:201
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
code_with_contract_typet::code_with_contract_typet
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
pointer_expr.h
API to expression classes for Pointers.
unsigned_long_long_int_type
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:101
c_bool_typet::c_bool_typet
c_bool_typet(std::size_t width)
Definition: c_types.h:64
code_with_contract_typet::ensures
exprt::operandst & ensures()
Definition: c_types.h:375
can_cast_type< c_enum_typet >
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
pointer_diff_type
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
c_enum_typet::c_enum_membert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: c_types.h:226
irept::swap
void swap(irept &irep)
Definition: irep.h:453
code_typet
Base type of functions.
Definition: std_types.h:539
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
union_typet
The union type.
Definition: c_types.h:112
tag_typet
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:396
can_cast_type< union_typet >
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
typet::check
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
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
c_enum_typet::c_enum_membert::get_value
irep_idt get_value() const
Definition: c_types.h:214
to_c_bit_field_type
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
void_type
empty_typet void_type()
Definition: c_types.cpp:253
c_enum_tag_typet::c_enum_tag_typet
c_enum_tag_typet(const irep_idt &identifier)
Definition: c_types.h:294
code_with_contract_typet
Definition: c_types.h:331
signed_size_type
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
code_with_contract_typet::has_contract
bool has_contract() const
Definition: c_types.h:342
unsigned_int_type
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:292
c_enum_typet::c_enum_membert
Definition: c_types.h:212
c_enum_typet::c_enum_membert::set_base_name
void set_base_name(const irep_idt &base_name)
Definition: c_types.h:234
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:832
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
char16_t_type
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:165
signed_long_long_int_type
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:87
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
code_with_contract_typet::ensures
const exprt::operandst & ensures() const
Definition: c_types.h:370
unsigned_char_type
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
code_with_contract_typet::requires
exprt::operandst & requires()
Definition: c_types.h:365
irept::get_sub
subt & get_sub()
Definition: irep.h:467
signed_long_int_type
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:80
unsigned_short_int_type
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:51
union_tag_typet::union_tag_typet
union_tag_typet(const irep_idt &identifier)
Definition: c_types.h:166
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
c_enum_typet::c_enum_membert::get_identifier
irep_idt get_identifier() const
Definition: c_types.h:222
signed_short_int_type
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:37
pointer_type
pointer_typet pointer_type(const typet &)
Definition: c_types.cpp:243
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
wchar_t_type
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
union_typet::union_typet
union_typet()
Definition: c_types.h:114
code_with_contract_typet::assigns
exprt & assigns()
Definition: c_types.h:352
code_with_contract_typet::requires
const exprt::operandst & requires() const
Definition: c_types.h:360
c_enum_typet::members
const memberst & members() const
Definition: c_types.h:242
can_cast_type< c_bit_field_typet >
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