cprover
c_types.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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{
21public:
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
44template <>
46{
47 return type.id() == ID_c_bit_field;
48}
49
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{
76public:
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
92template <>
93inline bool can_cast_type<c_bool_typet>(const typet &type)
94{
95 return type.id() == ID_c_bool;
96}
97
106inline const c_bool_typet &to_c_bool_type(const typet &type)
107{
110 return static_cast<const c_bool_typet &>(type);
111}
112
115{
118 return static_cast<c_bool_typet &>(type);
119}
120
125{
126public:
128 {
129 }
130
131 explicit union_typet(componentst _components)
132 : struct_union_typet(ID_union, std::move(_components))
133 {
134 }
135
143};
144
148template <>
149inline bool can_cast_type<union_typet>(const typet &type)
150{
151 return type.id() == ID_union;
152}
153
162inline 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{
178public:
179 explicit union_tag_typet(const irep_idt &identifier)
180 : tag_typet(ID_union_tag, identifier)
181 {
182 }
183};
184
188template <>
189inline bool can_cast_type<union_tag_typet>(const typet &type)
190{
191 return type.id() == ID_union_tag;
192}
193
202inline 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{
218public:
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
288template <>
289inline bool can_cast_type<c_enum_typet>(const typet &type)
290{
291 return type.id() == ID_c_enum;
292}
293
302inline 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{
320public:
321 explicit c_enum_tag_typet(const irep_idt &identifier)
322 : tag_typet(ID_c_enum_tag, identifier)
323 {
324 }
325};
326
330template <>
332{
333 return type.id() == ID_c_enum_tag;
334}
335
344inline 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{
359public:
364 code_with_contract_typet(parameterst _parameters, typet _return_type)
365 : code_typet(std::move(_parameters), std::move(_return_type))
366 {
367 }
368
370 {
371 return static_cast<const exprt &>(find(ID_C_spec_assigns)).operands();
372 }
373
375 {
376 return static_cast<exprt &>(add(ID_C_spec_assigns)).operands();
377 }
378
379 const exprt::operandst &requires() const
380 {
381 return static_cast<const exprt &>(find(ID_C_spec_requires)).operands();
382 }
383
384 exprt::operandst &requires()
385 {
386 return static_cast<exprt &>(add(ID_C_spec_requires)).operands();
387 }
388
390 {
391 return static_cast<const exprt &>(find(ID_C_spec_ensures)).operands();
392 }
393
395 {
396 return static_cast<exprt &>(add(ID_C_spec_ensures)).operands();
397 }
398};
399
403template <>
405{
406 return type.id() == ID_code;
407}
408
417inline const code_with_contract_typet &
419{
422 return static_cast<const code_with_contract_typet &>(type);
423}
424
427{
430 return static_cast<code_with_contract_typet &>(type);
431}
432
434 SINCE(2022, 1, 13, "use c_index_type() or array_typet::index_type() instead"))
436
437DEPRECATED(SINCE(2022, 1, 13, "use c_enum_constant_type() instead"))
439
465
466// This is for Java and C++
468
469// Turns an ID_C_c_type into a string, e.g.,
470// ID_signed_int gets "signed int".
471std::string c_type_as_string(const irep_idt &);
472
473#endif // CPROVER_UTIL_C_TYPES_H
floatbv_typet float_type()
Definition: c_types.cpp:195
bitvector_typet index_type()
Definition: c_types.cpp:22
signedbv_typet signed_long_int_type()
Definition: c_types.cpp:90
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_char_type()
Definition: c_types.cpp:152
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:54
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
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
unsignedbv_typet unsigned_long_long_int_type()
Definition: c_types.cpp:111
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:185
bitvector_typet c_enum_constant_type()
return type of enum constants
Definition: c_types.cpp:28
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
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:104
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 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:418
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:68
empty_typet void_type()
Definition: c_types.cpp:263
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:238
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:145
signedbv_typet signed_size_type()
Definition: c_types.cpp:84
bitvector_typet char_type()
Definition: c_types.cpp:124
signedbv_typet signed_long_long_int_type()
Definition: c_types.cpp:97
pointer_typet pointer_type(const typet &)
Definition: c_types.cpp:253
bitvector_typet wchar_t_type()
Definition: c_types.cpp:159
floatbv_typet long_double_type()
Definition: c_types.cpp:211
bitvector_typet enum_constant_type()
Definition: c_types.cpp:35
typet c_bool_type()
Definition: c_types.cpp:118
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:258
floatbv_typet double_type()
Definition: c_types.cpp:203
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:106
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:404
signedbv_typet signed_short_int_type()
Definition: c_types.cpp:47
unsignedbv_typet unsigned_short_int_type()
Definition: c_types.cpp:61
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:175
std::string c_type_as_string(const irep_idt &)
Definition: c_types.cpp:269
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
Base class of fixed-width bit-vector types.
Definition: std_types.h:853
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
const typet & underlying_type() const
Definition: c_types.h:30
typet & underlying_type()
Definition: c_types.h:35
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
const typet & underlying_type() const
Definition: c_types.h:274
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
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:542
exprt::operandst & assigns()
Definition: c_types.h:374
const exprt::operandst & assigns() const
Definition: c_types.h:369
exprt::operandst &const exprt::operandst & ensures() const
Definition: c_types.h:389
exprt::operandst & ensures()
Definition: c_types.h:394
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: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:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
subt & get_sub()
Definition: irep.h:456
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
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:149
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:168
const typet & subtype() const
Definition: type.h:156
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
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:103
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:318
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
STL namespace.
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