33 if(type.
id()==ID_merged_type)
38 else if(type.
id()==ID_signed)
40 else if(type.
id()==ID_unsigned)
42 else if(type.
id()==ID_ptr32)
44 else if(type.
id()==ID_ptr64)
46 else if(type.
id()==ID_volatile)
48 else if(type.
id()==ID_asm)
54 else if(type.
id()==ID_section &&
60 else if(type.
id()==ID_const)
62 else if(type.
id()==ID_restrict)
64 else if(type.
id()==ID_atomic)
66 else if(type.
id()==ID_atomic_type_specifier)
72 else if(type.
id()==ID_char)
74 else if(type.
id()==ID_int)
76 else if(type.
id()==ID_int8)
78 else if(type.
id()==ID_int16)
80 else if(type.
id()==ID_int32)
82 else if(type.
id()==ID_int64)
84 else if(type.
id()==ID_gcc_float16)
86 else if(type.
id()==ID_gcc_float32)
88 else if(type.
id()==ID_gcc_float32x)
90 else if(type.
id()==ID_gcc_float64)
92 else if(type.
id()==ID_gcc_float64x)
94 else if(type.
id()==ID_gcc_float128)
96 else if(type.
id()==ID_gcc_float128x)
98 else if(type.
id()==ID_gcc_int128)
100 else if(type.
id()==ID_gcc_attribute_mode)
104 else if(type.
id()==ID_msc_based)
106 const exprt &as_expr=
107 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
110 else if(type.
id()==ID_custom_bv)
113 const exprt &size_expr=
114 static_cast<const exprt &
>(type.
find(ID_size));
118 else if(type.
id()==ID_custom_floatbv)
122 const exprt &size_expr=
123 static_cast<const exprt &
>(type.
find(ID_size));
124 const exprt &fsize_expr=
125 static_cast<const exprt &
>(type.
find(ID_f));
130 else if(type.
id()==ID_custom_fixedbv)
134 const exprt &size_expr=
135 static_cast<const exprt &
>(type.
find(ID_size));
136 const exprt &fsize_expr=
137 static_cast<const exprt &
>(type.
find(ID_f));
142 else if(type.
id()==ID_short)
144 else if(type.
id()==ID_long)
146 else if(type.
id()==ID_double)
148 else if(type.
id()==ID_float)
150 else if(type.
id()==ID_c_bool)
152 else if(type.
id()==ID_proper_bool)
154 else if(type.
id()==ID_complex)
156 else if(type.
id()==ID_static)
158 else if(type.
id()==ID_thread_local)
160 else if(type.
id()==ID_inline)
162 else if(type.
id()==ID_extern)
164 else if(type.
id()==ID_typedef)
166 else if(type.
id()==ID_register)
168 else if(type.
id()==ID_weak)
170 else if(type.
id() == ID_used)
172 else if(type.
id()==ID_auto)
176 else if(type.
id()==ID_packed)
178 else if(type.
id()==ID_aligned)
188 else if(type.
id()==ID_transparent_union)
192 else if(type.
id()==ID_vector)
194 else if(type.
id()==ID_void)
199 other.push_back(tmp);
201 else if(type.
id()==ID_msc_declspec)
203 const exprt &as_expr=
204 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
209 const irep_idt &
id=it->get(ID_identifier);
220 else if(type.
id()==ID_noreturn)
222 else if(type.
id()==ID_constructor)
224 else if(type.
id()==ID_destructor)
226 else if(type.
id()==ID_alias &&
232 else if(type.
id()==ID_frontend_pointer)
239 const irep_idt typedef_identifier=type.
get(ID_C_typedef);
240 if(!typedef_identifier.
empty())
241 tmp.
set(ID_C_typedef, typedef_identifier);
242 other.push_back(tmp);
244 else if(type.
id()==ID_pointer)
249 other.push_back(type);
271 error() <<
"illegal type modifier for defined type" <<
eom;
278 if(
other.front().id()==ID_asm &&
other.back().id()==ID_empty)
280 else if(
other.front().id()==ID_empty &&
other.back().id()==ID_asm)
287 error() <<
"illegal combination of defined types" <<
eom;
298 error() <<
"combining constructor and destructor not supported"
304 if(type.
id()==ID_code)
307 else if(type_p->
id()!=ID_empty)
310 error() <<
"constructor and destructor required to be type void, "
321 error() <<
"constructor and destructor required to be type void, "
336 error() <<
"cannot combine integer type with floating-point type" <<
eom;
347 error() <<
"conflicting type modifiers" <<
eom;
377 error() <<
"cannot combine integer type with floating-point type" <<
eom;
384 error() <<
"conflicting type modifiers" <<
eom;
402 error() <<
"conflicting type modifiers" <<
eom;
409 error() <<
"illegal type modifier for float" <<
eom;
421 error() <<
"illegal type modifier for C boolean type" <<
eom;
435 error() <<
"illegal type modifier for proper boolean type" <<
eom;
454 error() <<
"illegal type modifier for char type" <<
eom;
461 error() <<
"conflicting type modifiers" <<
eom;
480 error() <<
"conflicting type modifiers" <<
eom;
493 error() <<
"conflicting type modifiers" <<
eom;
530 type.
id(
is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
535 type.
id(ID_custom_floatbv);
541 type.
id(ID_custom_fixedbv);
550 error() <<
"conflicting type modifiers" <<
eom;
583 error() <<
"illegal type modifier for integer type" <<
eom;
625 type.
set(ID_C_packed,
true);
ANSI-C Language Conversion.
floatbv_typet float_type()
signedbv_typet signed_long_int_type()
signedbv_typet signed_char_type()
unsignedbv_typet unsigned_int_type()
unsignedbv_typet unsigned_long_long_int_type()
unsignedbv_typet unsigned_long_int_type()
signedbv_typet signed_int_type()
unsignedbv_typet unsigned_char_type()
bitvector_typet char_type()
signedbv_typet signed_long_long_int_type()
floatbv_typet long_double_type()
floatbv_typet double_type()
signedbv_typet signed_short_int_type()
unsignedbv_typet unsigned_short_int_type()
virtual void read_rec(const typet &type)
c_storage_spect c_storage_spec
virtual void read(const typet &type)
virtual void write(typet &type)
unsigned gcc_float128x_cnt
unsigned gcc_float32x_cnt
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
unsigned gcc_float64x_cnt
source_locationt source_location
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
c_qualifierst c_qualifiers
unsigned gcc_float128_cnt
virtual void write(typet &src) const override
bool is_transparent_union
const typet & return_type() const
Complex numbers made of pair of given subtype.
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
const source_locationt & source_location() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void set(const irep_namet &name, const irep_idt &value)
const irept & find(const irep_namet &name) const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
source_locationt source_location
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const irep_idt & get_value() const
Type with a single subtype.
The type of an expression, extends irept.
const source_locationt & source_location() const
const typet & subtype() const
source_locationt & add_source_location()
const constant_exprt & size() const
#define forall_operands(it, expr)
floatbv_typet gcc_float32_type()
floatbv_typet gcc_float16_type()
floatbv_typet gcc_float64_type()
signedbv_typet gcc_signed_int128_type()
floatbv_typet gcc_float32x_type()
floatbv_typet gcc_float64x_type()
floatbv_typet gcc_float128x_type()
unsignedbv_typet gcc_unsigned_int128_type()
floatbv_typet gcc_float128_type()
#define UNREACHABLE
This should be used to mark dead code.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const string_constantt & to_string_constant(const exprt &expr)
std::size_t pointer_width
const type_with_subtypest & to_type_with_subtypes(const typet &type)
bool is_signed(const typet &t)
Convenience function – is the type signed?