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)
255 if(src_type.
id()!=ID_symbol)
258 typet result_type=src_type;
263 while(result_type.
id()==ID_symbol)
265 const symbolt &followed_type_symbol =
268 result_type=followed_type_symbol.
type;
272 qualifiers.
write(result_type);
278 const typet &type)
const 280 unsigned width=type.
get_int(ID_width);
282 if(type.
id()==ID_signedbv)
297 else if(type.
id()==ID_unsignedbv)
312 else if(type.
id()==ID_bool)
314 else if(type.
id()==ID_c_bool)
316 else if(type.
id()==ID_floatbv)
327 else if(type.
id()==ID_fixedbv)
331 else if(type.
id()==ID_pointer)
338 else if(type.
id()==ID_array)
342 else if(type.
id()==ID_c_enum ||
343 type.
id()==ID_c_enum_tag ||
344 type.
id()==ID_incomplete_c_enum)
348 else if(type.
id()==ID_symbol)
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");
566 warnings.push_back(
"disregarding volatile");
568 if(src_type==dest_type)
570 expr.
type()=src_type;
580 errors.push_back(
"implicit conversion not permitted");
581 else if(src_type!=dest_type)
595 c_typet max_type=std::max(c_type1, c_type2);
600 std::size_t width1=type1.
get_size_t(ID_width);
601 std::size_t width2=type2.
get_size_t(ID_width);
613 else if(width1>width2)
706 if(src_type.
id()==ID_array)
718 if(src_type!=dest_type)
725 if(dest_type.
get(ID_C_c_type)==ID_bool)
730 else if(dest_type.
id()==ID_bool)
The type of an expression.
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)
void do_typecast(exprt &dest, const typet &type)
Deprecated expression utility functions.
bool full_eq(const irept &other) const
unsignedbv_typet unsigned_int_type()
signed int get_int(const irep_namet &name) const
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
Unbounded, signed rational numbers.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
bitvector_typet double_type()
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
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
bitvector_typet float_type()
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
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
bitvector_typet index_type()
typet follow_with_qualifiers(const typet &src)
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)
bitvector_typet long_double_type()
Unbounded, signed integers.
typet type
Type of symbol.
virtual void implicit_typecast_arithmetic(exprt &expr)
bool is_number(const typet &type)
Unbounded, signed real numbers.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Base class for all expressions.
virtual void implicit_typecast(exprt &expr, const typet &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 generic typet to a union_typet.
bool is_void_pointer(const typet &type)
virtual void write(typet &src) const override
unsignedbv_typet unsigned_long_long_int_type()
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
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)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
std::size_t short_int_width
void set(const irep_namet &name, const irep_idt &value)
std::size_t long_double_width