29 const typet &dest_type,
34 return !c_typecast.
errors.empty();
38 const typet &src_type,
39 const typet &dest_type,
46 return !c_typecast.
errors.empty();
56 return !c_typecast.
errors.empty();
61 if(type.
id()==ID_pointer)
75 const typet &src_type,
76 const typet &dest_type)
81 src_type.
id() == ID_pointer && dest_type.
id() == ID_pointer &&
88 if(src_type==dest_type)
93 if(src_type_id==ID_c_bit_field)
99 if(dest_type.
id()==ID_c_bit_field)
105 if(src_type_id==ID_natural)
108 dest_type.
id() == ID_bool || dest_type.
id() == ID_c_bool ||
109 dest_type.
id() == ID_integer || dest_type.
id() == ID_rational ||
110 dest_type.
id() == ID_real || dest_type.
id() == ID_complex ||
111 dest_type.
id() == ID_unsignedbv || dest_type.
id() == ID_signedbv ||
112 dest_type.
id() == ID_floatbv || dest_type.
id() == ID_complex)
117 else if(src_type_id==ID_integer)
120 dest_type.
id() == ID_bool || dest_type.
id() == ID_c_bool ||
121 dest_type.
id() == ID_natural || dest_type.
id() == ID_rational ||
122 dest_type.
id() == ID_real || dest_type.
id() == ID_complex ||
123 dest_type.
id() == ID_unsignedbv || dest_type.
id() == ID_signedbv ||
124 dest_type.
id() == ID_floatbv || dest_type.
id() == ID_fixedbv ||
125 dest_type.
id() == ID_pointer || dest_type.
id() == ID_complex)
130 else if(src_type_id==ID_real)
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_rational)
143 dest_type.
id() == ID_bool || dest_type.
id() == ID_c_bool ||
144 dest_type.
id() == ID_real || dest_type.
id() == ID_complex ||
145 dest_type.
id() == ID_floatbv || dest_type.
id() == ID_fixedbv ||
146 dest_type.
id() == ID_complex)
151 else if(src_type_id==ID_bool)
154 dest_type.
id() == ID_c_bool || dest_type.
id() == ID_integer ||
155 dest_type.
id() == ID_natural || dest_type.
id() == ID_rational ||
156 dest_type.
id() == ID_real || dest_type.
id() == ID_unsignedbv ||
157 dest_type.
id() == ID_signedbv || dest_type.
id() == ID_pointer ||
158 dest_type.
id() == ID_floatbv || dest_type.
id() == ID_fixedbv ||
159 dest_type.
id() == ID_c_enum || dest_type.
id() == ID_c_enum_tag ||
160 dest_type.
id() == ID_complex)
165 else if(src_type_id==ID_unsignedbv ||
166 src_type_id==ID_signedbv ||
167 src_type_id==ID_c_enum ||
168 src_type_id==ID_c_enum_tag ||
169 src_type_id==ID_c_bool)
172 dest_type.
id() == ID_unsignedbv || dest_type.
id() == ID_bool ||
173 dest_type.
id() == ID_c_bool || dest_type.
id() == ID_integer ||
174 dest_type.
id() == ID_natural || dest_type.
id() == ID_rational ||
175 dest_type.
id() == ID_real || dest_type.
id() == ID_signedbv ||
176 dest_type.
id() == ID_floatbv || dest_type.
id() == ID_fixedbv ||
177 dest_type.
id() == ID_pointer || dest_type.
id() == ID_c_enum ||
178 dest_type.
id() == ID_c_enum_tag || dest_type.
id() == ID_complex)
183 else if(src_type_id==ID_floatbv ||
184 src_type_id==ID_fixedbv)
186 if(dest_type.
id()==ID_bool ||
187 dest_type.
id()==ID_c_bool ||
188 dest_type.
id()==ID_integer ||
189 dest_type.
id()==ID_real ||
190 dest_type.
id()==ID_rational ||
191 dest_type.
id()==ID_signedbv ||
192 dest_type.
id()==ID_unsignedbv ||
193 dest_type.
id()==ID_floatbv ||
194 dest_type.
id()==ID_fixedbv ||
195 dest_type.
id()==ID_complex)
198 else if(src_type_id==ID_complex)
200 if(dest_type.
id()==ID_complex)
219 else if(src_type_id==ID_array ||
220 src_type_id==ID_pointer)
222 if(dest_type.
id()==ID_pointer)
227 if(src_subtype == dest_subtype)
246 if(dest_type.
id()==ID_bool ||
247 dest_type.
id()==ID_c_bool ||
248 dest_type.
id()==ID_unsignedbv ||
249 dest_type.
id()==ID_signedbv)
252 else if(src_type_id==ID_vector)
254 if(dest_type.
id()==ID_vector)
257 else if(src_type_id==ID_complex)
259 if(dest_type.
id()==ID_complex)
278 src_type.
id() != ID_struct_tag &&
279 src_type.
id() != ID_union_tag)
284 typet result_type=src_type;
292 const typet &followed_type =
ns.follow_tag(*struct_tag_type);
293 result_type = followed_type;
299 const typet &followed_type =
ns.follow_tag(*union_tag_type);
300 result_type = followed_type;
304 qualifiers.
write(result_type);
310 const typet &type)
const
312 if(type.
id()==ID_signedbv)
316 if(width<=
config.ansi_c.char_width)
318 else if(width<=
config.ansi_c.short_int_width)
320 else if(width<=
config.ansi_c.int_width)
322 else if(width<=
config.ansi_c.long_int_width)
324 else if(width<=
config.ansi_c.long_long_int_width)
329 else if(type.
id()==ID_unsignedbv)
333 if(width<=
config.ansi_c.char_width)
335 else if(width<=
config.ansi_c.short_int_width)
337 else if(width<=
config.ansi_c.int_width)
339 else if(width<=
config.ansi_c.long_int_width)
341 else if(width<=
config.ansi_c.long_long_int_width)
346 else if(type.
id()==ID_bool)
348 else if(type.
id()==ID_c_bool)
350 else if(type.
id()==ID_floatbv)
354 if(width<=
config.ansi_c.single_width)
356 else if(width<=
config.ansi_c.double_width)
358 else if(width<=
config.ansi_c.long_double_width)
363 else if(type.
id()==ID_fixedbv)
367 else if(type.
id()==ID_pointer)
374 else if(type.
id()==ID_array)
378 else if(type.
id() == ID_c_enum || type.
id() == ID_c_enum_tag)
382 else if(type.
id()==ID_rational)
384 else if(type.
id()==ID_real)
386 else if(type.
id()==ID_complex)
388 else if(type.
id()==ID_c_bit_field)
394 typet underlying_type;
396 if(bit_field_type.underlying_type().id() == ID_c_enum_tag)
398 const auto &followed =
400 if(followed.is_incomplete())
403 underlying_type = followed.underlying_type();
406 underlying_type = bit_field_type.underlying_type();
409 underlying_type.
id(), bit_field_type.get_width());
413 else if(type.
id() == ID_integer)
415 else if(type.
id() == ID_natural)
430 if(expr.
type().
id() == ID_array)
468 if(new_type != expr.
type())
473 const typet &type)
const
489 config.ansi_c.short_int_width ==
config.ansi_c.int_width &&
497 type.
id()==ID_c_bit_field &&
517 typet type_qual=type;
519 qualifiers.
write(type_qual);
526 const typet &src_type,
527 const typet &orig_dest_type,
528 const typet &dest_type)
531 if(dest_type.
id()==ID_union &&
532 dest_type.
get_bool(ID_C_transparent_union) &&
533 src_type.
id()!=ID_union)
543 typet src_type_no_const=src_type;
545 src_type.
id() == ID_pointer &&
552 for(
const auto &comp :
to_union_type(dest_type).components())
557 union_exprt union_expr(comp.get_name(), expr, orig_dest_type);
558 if(!src_type.
full_eq(src_type_no_const))
566 if(dest_type.
id()==ID_pointer)
572 (src_type.
id() == ID_unsignedbv || src_type.
id() == ID_signedbv ||
573 src_type.
id() == ID_natural || src_type.
id() == ID_integer))
579 if(src_type.
id()==ID_pointer ||
580 src_type.
id()==ID_array)
591 else if(src_sub.
id()==ID_code &&
592 dest_sub.
id()==ID_code)
597 else if(src_sub == dest_sub)
602 src_sub.
id()==ID_c_enum ||
603 src_sub.
id()==ID_c_enum_tag) &&
605 dest_sub.
id()==ID_c_enum ||
606 src_sub.
id()==ID_c_enum_tag))
612 src_sub.
id() == ID_array && dest_sub.
id() == ID_array &&
620 warnings.push_back(
"incompatible pointer types");
628 warnings.push_back(
"disregarding volatile");
631 if(src_type==dest_type)
633 expr.
type()=src_type;
643 errors.push_back(
"implicit conversion not permitted");
644 else if(src_type!=dest_type)
658 c_typet max_type=std::max(c_type1, c_type2);
663 typet result_type = (max_type == c_type1) ? type1 : type2;
732 else if(max_type ==
OTHER)
734 errors.push_back(
"implicit arithmetic conversion not permitted");
749 if(src_type.
id()==ID_array)
754 if(error_opt.has_value())
756 errors.push_back(error_opt.value());
765 if(src_type!=dest_type)
772 if(dest_type.
get(ID_C_c_type)==ID_bool)
776 else if(dest_type.
id()==ID_bool)
780 else if(dest_type.
id() == ID_rational)
786 if(op1.has_value() && op2.has_value())
808std::optional<std::string>
811 if(type.
id() == ID_c_bit_field)
812 return std::string(
"cannot take address of a bit field");
814 if(type.
id() == ID_bool)
815 return std::string(
"cannot take address of a proper Boolean");
821 if(width %
config.ansi_c.char_width != 0)
824 "bitvector must have width that is a multiple of CHAR_BIT");
830 if(type.
id() == ID_array)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_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)
bool check_c_implicit_typecast(const typet &src_type, const typet &dest_type)
floatbv_typet float_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()
bitvector_typet c_index_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 c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Operator to return the address of an object.
const typet & element_type() const
The type of the elements of the array.
Base class of fixed-width bit-vector types.
std::size_t get_width() const
virtual void write(typet &src) const
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
static std::optional< std::string > check_address_can_be_taken(const typet &)
c_typet minimum_promotion(const typet &type) const
std::list< std::string > errors
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.
bool get_bool(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void remove(const irep_idt &name)
bool full_eq(const irept &other) const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Natural numbers including zero (mathematical integers, not bitvectors).
The null pointer constant.
const typet & base_type() const
The type of the data what we point to.
Unbounded, signed rational numbers.
Unbounded, signed real numbers.
const typet & subtype() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Union constructor from single element.
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const type_with_subtypet & to_type_with_subtype(const typet &type)