28 const typet &dest_type,
33 return !c_typecast.
errors.empty();
37 const typet &src_type,
38 const typet &dest_type,
45 return !c_typecast.
errors.empty();
55 return !c_typecast.
errors.empty();
60 if(type.
id()==ID_pointer)
72 const typet &src_type,
73 const typet &dest_type)
77 if(src_type.
id()==ID_pointer && dest_type.
id()==ID_pointer &&
82 if(src_type==dest_type)
87 if(src_type_id==ID_c_bit_field)
90 if(dest_type.
id()==ID_c_bit_field)
93 if(src_type_id==ID_natural)
95 if(dest_type.
id()==ID_bool ||
96 dest_type.
id()==ID_c_bool ||
97 dest_type.
id()==ID_integer ||
98 dest_type.
id()==ID_real ||
99 dest_type.
id()==ID_complex ||
100 dest_type.
id()==ID_unsignedbv ||
101 dest_type.
id()==ID_signedbv ||
102 dest_type.
id()==ID_floatbv ||
103 dest_type.
id()==ID_complex)
106 else if(src_type_id==ID_integer)
108 if(dest_type.
id()==ID_bool ||
109 dest_type.
id()==ID_c_bool ||
110 dest_type.
id()==ID_real ||
111 dest_type.
id()==ID_complex ||
112 dest_type.
id()==ID_unsignedbv ||
113 dest_type.
id()==ID_signedbv ||
114 dest_type.
id()==ID_floatbv ||
115 dest_type.
id()==ID_fixedbv ||
116 dest_type.
id()==ID_pointer ||
117 dest_type.
id()==ID_complex)
120 else if(src_type_id==ID_real)
122 if(dest_type.
id()==ID_bool ||
123 dest_type.
id()==ID_c_bool ||
124 dest_type.
id()==ID_complex ||
125 dest_type.
id()==ID_floatbv ||
126 dest_type.
id()==ID_fixedbv ||
127 dest_type.
id()==ID_complex)
130 else if(src_type_id==ID_rational)
132 if(dest_type.
id()==ID_bool ||
133 dest_type.
id()==ID_c_bool ||
134 dest_type.
id()==ID_complex ||
135 dest_type.
id()==ID_floatbv ||
136 dest_type.
id()==ID_fixedbv ||
137 dest_type.
id()==ID_complex)
140 else if(src_type_id==ID_bool)
142 if(dest_type.
id()==ID_c_bool ||
143 dest_type.
id()==ID_integer ||
144 dest_type.
id()==ID_real ||
145 dest_type.
id()==ID_unsignedbv ||
146 dest_type.
id()==ID_signedbv ||
147 dest_type.
id()==ID_pointer ||
148 dest_type.
id()==ID_floatbv ||
149 dest_type.
id()==ID_fixedbv ||
150 dest_type.
id()==ID_c_enum ||
151 dest_type.
id()==ID_c_enum_tag ||
152 dest_type.
id()==ID_complex)
155 else if(src_type_id==ID_unsignedbv ||
156 src_type_id==ID_signedbv ||
157 src_type_id==ID_c_enum ||
158 src_type_id==ID_c_enum_tag ||
159 src_type_id==ID_incomplete_c_enum ||
160 src_type_id==ID_c_bool)
162 if(dest_type.
id()==ID_unsignedbv ||
163 dest_type.
id()==ID_bool ||
164 dest_type.
id()==ID_c_bool ||
165 dest_type.
id()==ID_integer ||
166 dest_type.
id()==ID_real ||
167 dest_type.
id()==ID_rational ||
168 dest_type.
id()==ID_signedbv ||
169 dest_type.
id()==ID_floatbv ||
170 dest_type.
id()==ID_fixedbv ||
171 dest_type.
id()==ID_pointer ||
172 dest_type.
id()==ID_c_enum ||
173 dest_type.
id()==ID_c_enum_tag ||
174 dest_type.
id()==ID_incomplete_c_enum ||
175 dest_type.
id()==ID_complex)
178 else if(src_type_id==ID_floatbv ||
179 src_type_id==ID_fixedbv)
181 if(dest_type.
id()==ID_bool ||
182 dest_type.
id()==ID_c_bool ||
183 dest_type.
id()==ID_integer ||
184 dest_type.
id()==ID_real ||
185 dest_type.
id()==ID_rational ||
186 dest_type.
id()==ID_signedbv ||
187 dest_type.
id()==ID_unsignedbv ||
188 dest_type.
id()==ID_floatbv ||
189 dest_type.
id()==ID_fixedbv ||
190 dest_type.
id()==ID_complex)
193 else if(src_type_id==ID_complex)
195 if(dest_type.
id()==ID_complex)
209 else if(src_type_id==ID_array ||
210 src_type_id==ID_pointer)
212 if(dest_type.
id()==ID_pointer)
217 if(src_subtype==dest_subtype)
224 if(dest_type.
id()==ID_array &&
228 if(dest_type.
id()==ID_bool ||
229 dest_type.
id()==ID_c_bool ||
230 dest_type.
id()==ID_unsignedbv ||
231 dest_type.
id()==ID_signedbv)
234 else if(src_type_id==ID_vector)
236 if(dest_type.
id()==ID_vector)
239 else if(src_type_id==ID_complex)
241 if(dest_type.
id()==ID_complex)
256 src_type.
id() != ID_struct_tag &&
257 src_type.
id() != ID_union_tag)
262 typet result_type=src_type;
267 while(result_type.
id() == ID_struct_tag || result_type.
id() == ID_union_tag)
270 result_type = followed_type;
274 qualifiers.
write(result_type);
280 const typet &type)
const 282 const std::size_t width = type.
get_size_t(ID_width);
284 if(type.
id()==ID_signedbv)
299 else if(type.
id()==ID_unsignedbv)
314 else if(type.
id()==ID_bool)
316 else if(type.
id()==ID_c_bool)
318 else if(type.
id()==ID_floatbv)
329 else if(type.
id()==ID_fixedbv)
333 else if(type.
id()==ID_pointer)
340 else if(type.
id()==ID_array)
344 else if(type.
id()==ID_c_enum ||
345 type.
id()==ID_c_enum_tag ||
346 type.
id()==ID_incomplete_c_enum)
350 else if(type.
id()==ID_rational)
352 else if(type.
id()==ID_real)
354 else if(type.
id()==ID_complex)
356 else if(type.
id()==ID_c_bit_field)
373 if(expr_type.
id()==ID_array)
403 if(new_type!=expr_type)
408 const typet &type)
const 432 type.
id()==ID_c_bit_field &&
452 typet type_qual=type;
454 qualifiers.
write(type_qual);
461 const typet &src_type,
462 const typet &orig_dest_type,
463 const typet &dest_type)
466 if(dest_type.
id()==ID_union &&
467 dest_type.
get_bool(ID_C_transparent_union) &&
468 src_type.
id()!=ID_union)
478 typet src_type_no_const=src_type;
479 if(src_type.
id()==ID_pointer &&
484 for(
const auto &comp :
to_union_type(dest_type).components())
489 union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
490 if(!src_type.
full_eq(src_type_no_const))
498 if(dest_type.
id()==ID_pointer)
503 src_type.
id()==ID_unsignedbv ||
504 src_type.
id()==ID_signedbv ||
505 src_type.
id()==ID_natural ||
506 src_type.
id()==ID_integer))
508 expr=
exprt(ID_constant, orig_dest_type);
509 expr.
set(ID_value, ID_NULL);
513 if(src_type.
id()==ID_pointer ||
514 src_type.
id()==ID_array)
526 else if(src_sub.
id()==ID_code &&
527 dest_sub.
id()==ID_code)
537 src_sub.
id()==ID_c_enum ||
538 src_sub.
id()==ID_c_enum_tag) &&
540 dest_sub.
id()==ID_c_enum ||
541 src_sub.
id()==ID_c_enum_tag))
546 else if(src_sub.
id()==ID_array &&
547 dest_sub.
id()==ID_array &&
554 warnings.push_back(
"incompatible pointer types");
560 warnings.push_back(
"disregarding volatile");
562 if(src_type==dest_type)
564 expr.
type()=src_type;
574 errors.push_back(
"implicit conversion not permitted");
575 else if(src_type!=dest_type)
589 c_typet max_type=std::max(c_type1, c_type2);
594 std::size_t width1=type1.
get_size_t(ID_width);
595 std::size_t width2=type2.
get_size_t(ID_width);
607 else if(width1>width2)
700 if(src_type.
id()==ID_array)
712 if(src_type!=dest_type)
719 if(dest_type.
get(ID_C_c_type)==ID_bool)
724 else if(dest_type.
id()==ID_bool)
The type of an expression, extends irept.
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
pointer_typet pointer_type(const typet &subtype)
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
void do_typecast(exprt &dest, const typet &type)
Deprecated expression utility functions.
bool full_eq(const irept &other) const
unsignedbv_typet unsigned_int_type()
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
Unbounded, signed rational numbers.
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
typet & type()
Return the type of the expression.
c_typet get_c_type(const typet &type) const
bool get_bool(const irep_namet &name) const
class floatbv_typet to_type() const
const irep_idt & id() const
std::size_t long_long_int_width
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
static ieee_float_spect quadruple_precision()
Fixed-width bit-vector with two's complement interpretation.
std::list< std::string > warnings
Union constructor from single element.
API to expression classes.
const irep_idt & get(const irep_namet &name) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
signedbv_typet signed_long_int_type()
Base class for tree-like data structures with sharing.
std::list< std::string > errors
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
typet follow_with_qualifiers(const typet &src)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Operator to return the address of an object.
std::size_t get_width() const
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
Unbounded, signed integers (mathematical integers, not bitvectors)
floatbv_typet long_double_type()
floatbv_typet float_type()
virtual void implicit_typecast_arithmetic(exprt &expr)
Unbounded, signed real numbers.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Base class for all expressions.
virtual void implicit_typecast(exprt &expr, const typet &type)
floatbv_typet double_type()
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
#define UNREACHABLE
This should be used to mark dead code.
bool is_void_pointer(const typet &type)
virtual void write(typet &src) const override
bool is_zero() const
Return whether the expression is a constant representing 0.
unsignedbv_typet unsigned_long_long_int_type()
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
signedbv_typet signed_int_type()
void remove(const irep_namet &name)
const typet & subtype() const
unsignedbv_typet unsigned_long_int_type()
signedbv_typet signed_long_long_int_type()
std::size_t long_int_width
std::size_t get_size_t(const irep_namet &name) const
c_typet minimum_promotion(const typet &type) const
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
std::size_t short_int_width
void set(const irep_namet &name, const irep_idt &value)
std::size_t long_double_width