Go to the documentation of this file.
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_c_bool)
161 if(dest_type.
id()==ID_unsignedbv ||
162 dest_type.
id()==ID_bool ||
163 dest_type.
id()==ID_c_bool ||
164 dest_type.
id()==ID_integer ||
165 dest_type.
id()==ID_real ||
166 dest_type.
id()==ID_rational ||
167 dest_type.
id()==ID_signedbv ||
168 dest_type.
id()==ID_floatbv ||
169 dest_type.
id()==ID_fixedbv ||
170 dest_type.
id()==ID_pointer ||
171 dest_type.
id()==ID_c_enum ||
172 dest_type.
id()==ID_c_enum_tag ||
173 dest_type.
id()==ID_complex)
176 else if(src_type_id==ID_floatbv ||
177 src_type_id==ID_fixedbv)
179 if(dest_type.
id()==ID_bool ||
180 dest_type.
id()==ID_c_bool ||
181 dest_type.
id()==ID_integer ||
182 dest_type.
id()==ID_real ||
183 dest_type.
id()==ID_rational ||
184 dest_type.
id()==ID_signedbv ||
185 dest_type.
id()==ID_unsignedbv ||
186 dest_type.
id()==ID_floatbv ||
187 dest_type.
id()==ID_fixedbv ||
188 dest_type.
id()==ID_complex)
191 else if(src_type_id==ID_complex)
193 if(dest_type.
id()==ID_complex)
207 else if(src_type_id==ID_array ||
208 src_type_id==ID_pointer)
210 if(dest_type.
id()==ID_pointer)
215 if(src_subtype == dest_subtype)
227 if(dest_type.
id()==ID_array &&
231 if(dest_type.
id()==ID_bool ||
232 dest_type.
id()==ID_c_bool ||
233 dest_type.
id()==ID_unsignedbv ||
234 dest_type.
id()==ID_signedbv)
237 else if(src_type_id==ID_vector)
239 if(dest_type.
id()==ID_vector)
242 else if(src_type_id==ID_complex)
244 if(dest_type.
id()==ID_complex)
259 src_type.
id() != ID_struct_tag &&
260 src_type.
id() != ID_union_tag)
265 typet result_type=src_type;
270 while(result_type.
id() == ID_struct_tag || result_type.
id() == ID_union_tag)
273 result_type = followed_type;
277 qualifiers.
write(result_type);
283 const typet &type)
const
285 if(type.
id()==ID_signedbv)
302 else if(type.
id()==ID_unsignedbv)
319 else if(type.
id()==ID_bool)
321 else if(type.
id()==ID_c_bool)
323 else if(type.
id()==ID_floatbv)
336 else if(type.
id()==ID_fixedbv)
340 else if(type.
id()==ID_pointer)
347 else if(type.
id()==ID_array)
351 else if(type.
id() == ID_c_enum || type.
id() == ID_c_enum_tag)
355 else if(type.
id()==ID_rational)
357 else if(type.
id()==ID_real)
359 else if(type.
id()==ID_complex)
361 else if(type.
id()==ID_c_bit_field)
367 typet underlying_type;
369 if(bit_field_type.subtype().id() == ID_c_enum_tag)
371 const auto &followed =
373 if(followed.is_incomplete())
376 underlying_type = followed.
subtype();
379 underlying_type = bit_field_type.
subtype();
382 underlying_type.
id(), bit_field_type.get_width());
399 if(expr.
type().
id() == ID_array)
434 if(new_type != expr.
type())
439 const typet &type)
const
463 type.
id()==ID_c_bit_field &&
483 typet type_qual=type;
485 qualifiers.
write(type_qual);
492 const typet &src_type,
493 const typet &orig_dest_type,
494 const typet &dest_type)
497 if(dest_type.
id()==ID_union &&
498 dest_type.
get_bool(ID_C_transparent_union) &&
499 src_type.
id()!=ID_union)
509 typet src_type_no_const=src_type;
510 if(src_type.
id()==ID_pointer &&
515 for(
const auto &comp :
to_union_type(dest_type).components())
520 union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
521 if(!src_type.
full_eq(src_type_no_const))
529 if(dest_type.
id()==ID_pointer)
534 src_type.
id()==ID_unsignedbv ||
535 src_type.
id()==ID_signedbv ||
536 src_type.
id()==ID_natural ||
537 src_type.
id()==ID_integer))
539 expr=
exprt(ID_constant, orig_dest_type);
540 expr.
set(ID_value, ID_NULL);
544 if(src_type.
id()==ID_pointer ||
545 src_type.
id()==ID_array)
556 else if(src_sub.
id()==ID_code &&
557 dest_sub.
id()==ID_code)
562 else if(src_sub == dest_sub)
567 src_sub.
id()==ID_c_enum ||
568 src_sub.
id()==ID_c_enum_tag) &&
570 dest_sub.
id()==ID_c_enum ||
571 src_sub.
id()==ID_c_enum_tag))
577 src_sub.
id() == ID_array && dest_sub.
id() == ID_array &&
584 warnings.push_back(
"incompatible pointer types");
590 warnings.push_back(
"disregarding volatile");
592 if(src_type==dest_type)
594 expr.
type()=src_type;
604 errors.push_back(
"implicit conversion not permitted");
605 else if(src_type!=dest_type)
619 c_typet max_type=std::max(c_type1, c_type2);
637 else if(width1>width2)
730 if(src_type.
id()==ID_array)
737 if(src_type!=dest_type)
744 if(dest_type.
get(ID_C_c_type)==ID_bool)
748 else if(dest_type.
id()==ID_bool)
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
static exprt conditional_cast(const exprt &expr, const typet &type)
const typet & subtype() const
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
signedbv_typet signed_long_long_int_type()
Unbounded, signed rational numbers.
bool full_eq(const irept &other) const
The type of an expression, extends irept.
floatbv_typet long_double_type()
Union constructor from single element.
Unbounded, signed integers (mathematical integers, not bitvectors)
Base class for all expressions.
static ieee_float_spect quadruple_precision()
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
bool c_implicit_typecast_arithmetic(exprt &expr1, exprt &expr2, const namespacet &ns)
perform arithmetic prompotions and conversions
c_typet minimum_promotion(const typet &type) const
struct configt::ansi_ct ansi_c
bitvector_typet index_type()
Fixed-width bit-vector with unsigned binary interpretation.
unsignedbv_typet unsigned_long_long_int_type()
unsignedbv_typet unsigned_long_int_type()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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
std::list< std::string > warnings
Unbounded, signed real numbers.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
signedbv_typet signed_int_type()
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type, const namespacet &ns)
class floatbv_typet to_type() const
Fixed-width bit-vector with two's complement interpretation.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
virtual void write(typet &src) const override
floatbv_typet float_type()
std::size_t long_long_int_width
exprt simplify_expr(exprt src, const namespacet &ns)
pointer_typet pointer_type(const typet &subtype)
unsignedbv_typet unsigned_int_type()
const irep_idt & id() const
void remove(const irep_namet &name)
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
virtual void implicit_typecast_followed(exprt &expr, const typet &src_type, const typet &orig_dest_type, const typet &dest_type)
floatbv_typet double_type()
std::size_t get_width() const
Deprecated expression utility functions.
bool has_a_void_pointer(const typet &type)
virtual void implicit_typecast_arithmetic(exprt &expr)
Base class of fixed-width bit-vector types.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
void set(const irep_namet &name, const irep_idt &value)
std::list< std::string > errors
std::size_t long_double_width
std::size_t short_int_width
signedbv_typet signed_long_int_type()
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Operator to return the address of an object.
Semantic type conversion.
virtual void implicit_typecast(exprt &expr, const typet &type)
typet follow_with_qualifiers(const typet &src)
void do_typecast(exprt &dest, const typet &type)
API to expression classes.
std::size_t long_int_width
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.