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)
375 new_type.
id(ID_pointer);
381 case BOOL: assert(
false);
382 case CHAR: assert(
false);
383 case UCHAR: assert(
false);
384 case SHORT: assert(
false);
385 case USHORT: assert(
false);
404 if(new_type!=expr_type)
409 const typet &type)
const 431 max_type=std::max(max_type,
INT);
434 type.
id()==ID_c_bit_field &&
454 typet type_qual=type;
456 qualifiers.
write(type_qual);
463 const typet &src_type,
464 const typet &orig_dest_type,
465 const typet &dest_type)
468 if(dest_type.
id()==ID_union &&
469 dest_type.
get_bool(ID_C_transparent_union) &&
470 src_type.
id()!=ID_union)
480 typet src_type_no_const=src_type;
481 if(src_type.
id()==ID_pointer &&
486 for(
const auto &comp :
to_union_type(dest_type).components())
491 exprt union_expr(ID_union, orig_dest_type);
493 if(!src_type.
full_eq(src_type_no_const))
495 union_expr.
set(ID_component_name, comp.get_name());
502 if(dest_type.
id()==ID_pointer)
507 src_type.
id()==ID_unsignedbv ||
508 src_type.
id()==ID_signedbv ||
509 src_type.
id()==ID_natural ||
510 src_type.
id()==ID_integer))
512 expr=
exprt(ID_constant, orig_dest_type);
513 expr.
set(ID_value, ID_NULL);
517 if(src_type.
id()==ID_pointer ||
518 src_type.
id()==ID_array)
530 else if(src_sub.
id()==ID_code &&
531 dest_sub.
id()==ID_code)
541 src_sub.
id()==ID_c_enum ||
542 src_sub.
id()==ID_c_enum_tag) &&
544 dest_sub.
id()==ID_c_enum ||
545 src_sub.
id()==ID_c_enum_tag))
551 warnings.push_back(
"incompatible pointer types");
563 warnings.push_back(
"disregarding volatile");
565 if(src_type==dest_type)
567 expr.
type()=src_type;
577 errors.push_back(
"implicit conversion not permitted");
578 else if(src_type!=dest_type)
592 c_typet max_type=std::max(c_type1, c_type2);
597 std::size_t width1=type1.
get_size_t(ID_width);
598 std::size_t width2=type2.
get_size_t(ID_width);
610 else if(width1>width2)
703 if(src_type.
id()==ID_array)
715 if(src_type!=dest_type)
722 if(dest_type.
get(ID_C_c_type)==ID_bool)
727 else if(dest_type.
id()==ID_bool)
The type of an expression.
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
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()
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
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.
void move_to_operands(exprt &expr)
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
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()
unsigned long_long_int_width
Fixed-width bit-vector with two's complement interpretation.
std::list< std::string > warnings
void write(typet &src) const
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 c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
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)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
bool is_number(const typet &type)
Unbounded, signed real numbers.
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
unsigned long_double_width
bool is_void_pointer(const typet &type)
unsignedbv_typet unsigned_long_long_int_type()
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 get_size_t(const irep_namet &name) const
c_typet minimum_promotion(const typet &type) const
void make_typecast(const typet &_type)
void set(const irep_namet &name, const irep_idt &value)