27 const typet &dest_type,
32 return !c_typecast.
errors.empty();
36 const typet &src_type,
37 const typet &dest_type,
44 return !c_typecast.
errors.empty();
54 return !c_typecast.
errors.empty();
59 if(type.
id()==ID_pointer)
71 const typet &src_type,
72 const typet &dest_type)
76 if(src_type.
id()==ID_pointer && dest_type.
id()==ID_pointer &&
81 if(src_type==dest_type)
86 if(src_type_id==ID_c_bit_field)
89 if(dest_type.
id()==ID_c_bit_field)
92 if(src_type_id==ID_natural)
94 if(dest_type.
id()==ID_bool ||
95 dest_type.
id()==ID_c_bool ||
96 dest_type.
id()==ID_integer ||
97 dest_type.
id()==ID_real ||
98 dest_type.
id()==ID_complex ||
99 dest_type.
id()==ID_unsignedbv ||
100 dest_type.
id()==ID_signedbv ||
101 dest_type.
id()==ID_floatbv ||
102 dest_type.
id()==ID_complex)
105 else if(src_type_id==ID_integer)
107 if(dest_type.
id()==ID_bool ||
108 dest_type.
id()==ID_c_bool ||
109 dest_type.
id()==ID_real ||
110 dest_type.
id()==ID_complex ||
111 dest_type.
id()==ID_unsignedbv ||
112 dest_type.
id()==ID_signedbv ||
113 dest_type.
id()==ID_floatbv ||
114 dest_type.
id()==ID_fixedbv ||
115 dest_type.
id()==ID_pointer ||
116 dest_type.
id()==ID_complex)
119 else if(src_type_id==ID_real)
121 if(dest_type.
id()==ID_bool ||
122 dest_type.
id()==ID_c_bool ||
123 dest_type.
id()==ID_complex ||
124 dest_type.
id()==ID_floatbv ||
125 dest_type.
id()==ID_fixedbv ||
126 dest_type.
id()==ID_complex)
129 else if(src_type_id==ID_rational)
131 if(dest_type.
id()==ID_bool ||
132 dest_type.
id()==ID_c_bool ||
133 dest_type.
id()==ID_complex ||
134 dest_type.
id()==ID_floatbv ||
135 dest_type.
id()==ID_fixedbv ||
136 dest_type.
id()==ID_complex)
139 else if(src_type_id==ID_bool)
141 if(dest_type.
id()==ID_c_bool ||
142 dest_type.
id()==ID_integer ||
143 dest_type.
id()==ID_real ||
144 dest_type.
id()==ID_unsignedbv ||
145 dest_type.
id()==ID_signedbv ||
146 dest_type.
id()==ID_pointer ||
147 dest_type.
id()==ID_floatbv ||
148 dest_type.
id()==ID_fixedbv ||
149 dest_type.
id()==ID_c_enum ||
150 dest_type.
id()==ID_c_enum_tag ||
151 dest_type.
id()==ID_complex)
154 else if(src_type_id==ID_unsignedbv ||
155 src_type_id==ID_signedbv ||
156 src_type_id==ID_c_enum ||
157 src_type_id==ID_c_enum_tag ||
158 src_type_id==ID_c_bool)
160 if(dest_type.
id()==ID_unsignedbv ||
161 dest_type.
id()==ID_bool ||
162 dest_type.
id()==ID_c_bool ||
163 dest_type.
id()==ID_integer ||
164 dest_type.
id()==ID_real ||
165 dest_type.
id()==ID_rational ||
166 dest_type.
id()==ID_signedbv ||
167 dest_type.
id()==ID_floatbv ||
168 dest_type.
id()==ID_fixedbv ||
169 dest_type.
id()==ID_pointer ||
170 dest_type.
id()==ID_c_enum ||
171 dest_type.
id()==ID_c_enum_tag ||
172 dest_type.
id()==ID_complex)
175 else if(src_type_id==ID_floatbv ||
176 src_type_id==ID_fixedbv)
178 if(dest_type.
id()==ID_bool ||
179 dest_type.
id()==ID_c_bool ||
180 dest_type.
id()==ID_integer ||
181 dest_type.
id()==ID_real ||
182 dest_type.
id()==ID_rational ||
183 dest_type.
id()==ID_signedbv ||
184 dest_type.
id()==ID_unsignedbv ||
185 dest_type.
id()==ID_floatbv ||
186 dest_type.
id()==ID_fixedbv ||
187 dest_type.
id()==ID_complex)
190 else if(src_type_id==ID_complex)
192 if(dest_type.
id()==ID_complex)
206 else if(src_type_id==ID_array ||
207 src_type_id==ID_pointer)
209 if(dest_type.
id()==ID_pointer)
214 if(src_subtype == dest_subtype)
226 if(dest_type.
id()==ID_array &&
230 if(dest_type.
id()==ID_bool ||
231 dest_type.
id()==ID_c_bool ||
232 dest_type.
id()==ID_unsignedbv ||
233 dest_type.
id()==ID_signedbv)
236 else if(src_type_id==ID_vector)
238 if(dest_type.
id()==ID_vector)
241 else if(src_type_id==ID_complex)
243 if(dest_type.
id()==ID_complex)
258 src_type.
id() != ID_struct_tag &&
259 src_type.
id() != ID_union_tag)
264 typet result_type=src_type;
269 while(result_type.
id() == ID_struct_tag || result_type.
id() == ID_union_tag)
272 result_type = followed_type;
276 qualifiers.
write(result_type);
282 const typet &type)
const
284 if(type.
id()==ID_signedbv)
301 else if(type.
id()==ID_unsignedbv)
318 else if(type.
id()==ID_bool)
320 else if(type.
id()==ID_c_bool)
322 else if(type.
id()==ID_floatbv)
335 else if(type.
id()==ID_fixedbv)
339 else if(type.
id()==ID_pointer)
346 else if(type.
id()==ID_array)
350 else if(type.
id() == ID_c_enum || type.
id() == ID_c_enum_tag)
354 else if(type.
id()==ID_rational)
356 else if(type.
id()==ID_real)
358 else if(type.
id()==ID_complex)
360 else if(type.
id()==ID_c_bit_field)
366 typet underlying_type;
368 if(bit_field_type.subtype().id() == ID_c_enum_tag)
370 const auto &followed =
372 if(followed.is_incomplete())
375 underlying_type = followed.
subtype();
378 underlying_type = bit_field_type.
subtype();
381 underlying_type.
id(), bit_field_type.get_width());
398 if(expr.
type().
id() == ID_array)
433 if(new_type != expr.
type())
438 const typet &type)
const
462 type.
id()==ID_c_bit_field &&
482 typet type_qual=type;
484 qualifiers.
write(type_qual);
491 const typet &src_type,
492 const typet &orig_dest_type,
493 const typet &dest_type)
496 if(dest_type.
id()==ID_union &&
497 dest_type.
get_bool(ID_C_transparent_union) &&
498 src_type.
id()!=ID_union)
508 typet src_type_no_const=src_type;
509 if(src_type.
id()==ID_pointer &&
514 for(
const auto &comp :
to_union_type(dest_type).components())
519 union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
520 if(!src_type.
full_eq(src_type_no_const))
528 if(dest_type.
id()==ID_pointer)
533 src_type.
id()==ID_unsignedbv ||
534 src_type.
id()==ID_signedbv ||
535 src_type.
id()==ID_natural ||
536 src_type.
id()==ID_integer))
538 expr=
exprt(ID_constant, orig_dest_type);
539 expr.
set(ID_value, ID_NULL);
543 if(src_type.
id()==ID_pointer ||
544 src_type.
id()==ID_array)
555 else if(src_sub.
id()==ID_code &&
556 dest_sub.
id()==ID_code)
561 else if(src_sub == dest_sub)
566 src_sub.
id()==ID_c_enum ||
567 src_sub.
id()==ID_c_enum_tag) &&
569 dest_sub.
id()==ID_c_enum ||
570 src_sub.
id()==ID_c_enum_tag))
576 src_sub.
id() == ID_array && dest_sub.
id() == ID_array &&
583 warnings.push_back(
"incompatible pointer types");
589 warnings.push_back(
"disregarding volatile");
591 if(src_type==dest_type)
593 expr.
type()=src_type;
603 errors.push_back(
"implicit conversion not permitted");
604 else if(src_type!=dest_type)
618 c_typet max_type=std::max(c_type1, c_type2);
636 else if(width1>width2)
704 else if(max_type ==
OTHER)
706 errors.push_back(
"implicit arithmetic conversion not permitted");
721 if(src_type.
id()==ID_array)
728 if(src_type!=dest_type)
735 if(dest_type.
get(ID_C_c_type)==ID_bool)
739 else if(dest_type.
id()==ID_bool)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
bool has_a_void_pointer(const typet &type)
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
floatbv_typet float_type()
bitvector_typet index_type()
signedbv_typet signed_long_int_type()
unsignedbv_typet unsigned_int_type()
unsignedbv_typet unsigned_long_long_int_type()
unsignedbv_typet unsigned_long_int_type()
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
signedbv_typet signed_long_long_int_type()
floatbv_typet long_double_type()
floatbv_typet double_type()
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Operator to return the address of an object.
Base class of fixed-width bit-vector types.
std::size_t get_width() const
virtual void write(typet &src) const override
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
typet follow_with_qualifiers(const typet &src)
void do_typecast(exprt &dest, const typet &type)
virtual void implicit_typecast(exprt &expr, const typet &type)
c_typet get_c_type(const typet &type) const
virtual void implicit_typecast_arithmetic(exprt &expr)
std::list< std::string > warnings
c_typet minimum_promotion(const typet &type) const
std::list< std::string > errors
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.
typet & type()
Return the type of the expression.
static ieee_float_spect quadruple_precision()
class floatbv_typet to_type() const
Unbounded, signed integers (mathematical integers, not bitvectors)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
void set(const irep_namet &name, const irep_idt &value)
bool get_bool(const irep_namet &name) const
const irep_idt & id() const
bool full_eq(const irept &other) const
void remove(const irep_namet &name)
const irep_idt & get(const irep_namet &name) const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Unbounded, signed rational numbers.
Unbounded, signed real numbers.
Fixed-width bit-vector with two's complement interpretation.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Deprecated expression utility functions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
API to expression classes for Pointers.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
API to expression classes.
std::size_t long_double_width
std::size_t long_long_int_width
std::size_t long_int_width
std::size_t short_int_width