24 if(type.
id()==ID_merged_type)
29 else if(type.
id()==ID_signed)
31 else if(type.
id()==ID_unsigned)
33 else if(type.
id()==ID_ptr32)
35 else if(type.
id()==ID_ptr64)
37 else if(type.
id()==ID_volatile)
39 else if(type.
id()==ID_asm)
44 !type_with_subtypes.subtypes().empty() &&
45 type_with_subtypes.subtypes()[0].id() == ID_string_constant)
56 else if(type.
id()==ID_const)
58 else if(type.
id()==ID_restrict)
60 else if(type.
id()==ID_atomic)
62 else if(type.
id()==ID_atomic_type_specifier)
68 else if(type.
id()==ID_char)
70 else if(type.
id()==ID_int)
72 else if(type.
id()==ID_int8)
74 else if(type.
id()==ID_int16)
76 else if(type.
id()==ID_int32)
78 else if(type.
id()==ID_int64)
80 else if(type.
id() == ID_c_bitint)
83 const exprt &size_expr =
static_cast<const exprt &
>(type.
find(ID_size));
87 else if(type.
id()==ID_gcc_float16)
89 else if(type.
id()==ID_gcc_float32)
91 else if(type.
id()==ID_gcc_float32x)
93 else if(type.
id()==ID_gcc_float64)
95 else if(type.
id()==ID_gcc_float64x)
97 else if(type.
id()==ID_gcc_float128)
99 else if(type.
id()==ID_gcc_float128x)
101 else if(type.
id()==ID_gcc_int128)
103 else if(type.
id()==ID_gcc_attribute_mode)
107 else if(type.
id()==ID_msc_based)
109 const exprt &as_expr=
110 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
113 else if(type.
id()==ID_custom_bv)
116 const exprt &size_expr=
117 static_cast<const exprt &
>(type.
find(ID_size));
121 else if(type.
id()==ID_custom_floatbv)
125 const exprt &size_expr=
126 static_cast<const exprt &
>(type.
find(ID_size));
127 const exprt &fsize_expr=
128 static_cast<const exprt &
>(type.
find(ID_f));
133 else if(type.
id()==ID_custom_fixedbv)
137 const exprt &size_expr=
138 static_cast<const exprt &
>(type.
find(ID_size));
139 const exprt &fsize_expr=
140 static_cast<const exprt &
>(type.
find(ID_f));
145 else if(type.
id()==ID_short)
147 else if(type.
id()==ID_long)
149 else if(type.
id()==ID_double)
151 else if(type.
id()==ID_float)
153 else if(type.
id()==ID_c_bool)
155 else if(type.
id()==ID_proper_bool)
157 else if(type.
id()==ID_complex)
159 else if(type.
id()==ID_static)
161 else if(type.
id()==ID_thread_local)
163 else if(type.
id()==ID_inline)
165 else if(type.
id()==ID_extern)
167 else if(type.
id()==ID_typedef)
169 else if(type.
id()==ID_register)
171 else if(type.
id()==ID_weak)
173 else if(type.
id() == ID_used)
175 else if(type.
id()==ID_auto)
179 else if(type.
id()==ID_packed)
181 else if(type.
id()==ID_aligned)
191 else if(type.
id()==ID_transparent_union)
195 else if(type.
id() == ID_frontend_vector)
200 else if(type.
id()==ID_void)
205 other.push_back(tmp);
207 else if(type.
id()==ID_msc_declspec)
209 const exprt &as_expr=
210 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
212 for(
const auto &op : as_expr.
operands())
215 const irep_idt &
id = op.get(ID_identifier);
226 else if(type.
id() == ID_nodiscard)
228 else if(type.
id()==ID_noreturn)
230 else if(type.
id()==ID_constructor)
232 else if(type.
id()==ID_destructor)
241 else if(type.
id()==ID_frontend_pointer)
249 const irep_idt typedef_identifier=type.
get(ID_C_typedef);
250 if(!typedef_identifier.
empty())
251 tmp.
set(ID_C_typedef, typedef_identifier);
252 other.push_back(tmp);
254 else if(type.
id()==ID_pointer)
258 else if(type.
id() == ID_C_spec_requires)
260 const exprt &as_expr =
261 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
264 else if(type.
id() == ID_C_spec_assigns)
266 const exprt &as_expr =
267 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
272 else if(type.
id() == ID_C_spec_frees)
274 const exprt &as_expr =
275 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
280 else if(type.
id() == ID_C_spec_ensures)
282 const exprt &as_expr =
283 static_cast<const exprt &
>(
static_cast<const irept &
>(type));
287 other.push_back(type);
316 if(
other.front().id()==ID_asm &&
other.back().id()==ID_empty)
318 else if(
other.front().id()==ID_empty &&
other.back().id()==ID_asm)
349 log.
error() <<
"combining constructor and destructor not supported"
355 if(type.
id()==ID_code)
358 else if(type_p->
id()!=ID_empty)
361 log.
error() <<
"constructor and destructor required to be type void, "
372 log.
error() <<
"constructor and destructor required to be type void, "
387 log.
error() <<
"cannot combine integer type with floating-point type"
429 log.
error() <<
"cannot combine integer type with floating-point type"
474 log.
error() <<
"illegal type modifier for C boolean type"
489 log.
error() <<
"illegal type modifier for proper boolean type"
587 type.
id(
is_signed ? ID_c_signed_bitint : ID_c_unsigned_bitint);
593 type.
id(
is_signed?ID_custom_signedbv:ID_custom_unsignedbv);
598 type.
id(ID_custom_floatbv);
604 type.
id(ID_custom_fixedbv);
688 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()
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
virtual void read_rec(const typet &type)
c_storage_spect c_storage_spec
exprt::operandst c_ensures
virtual void write(typet &type)
unsigned gcc_float128x_cnt
unsigned gcc_float32x_cnt
message_handlert & message_handler
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
unsigned gcc_float64x_cnt
exprt::operandst c_requires
source_locationt source_location
exprt::operandst c_assigns
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
const typet & return_type() const
const exprt::operandst & c_frees() const
const exprt::operandst & c_assigns() const
const exprt::operandst & c_requires() const
const exprt::operandst & c_ensures() const
Complex numbers made of pair of given subtype.
A constant literal expression.
Base class for all expressions.
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
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void value(const irep_idt &)
Type with a single subtype.
The type of an expression, extends irept.
source_locationt & add_source_location()
const source_locationt & source_location() const
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 code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const string_constantt & to_string_constant(const exprt &expr)
const type_with_subtypest & to_type_with_subtypes(const typet &type)
const type_with_subtypet & to_type_with_subtype(const typet &type)
bool is_signed(const typet &t)
Convenience function – is the type signed?