47 exprt &new_expr)
const 51 if(expr.
type().
id()==ID_code ||
52 expr.
type().
id()==ID_incomplete_struct ||
53 expr.
type().
id()==ID_incomplete_union)
57 new_expr.
remove(ID_C_lvalue);
72 exprt &new_expr)
const 74 assert(expr.
type().
id()==ID_array);
80 index.set(ID_C_lvalue,
true);
113 exprt &new_expr)
const 115 if(expr.
type().
id()!=ID_pointer ||
122 if(expr.
type()!=type)
129 while(sub_from.
id()==ID_pointer)
140 if(qual_from!=qual_to && !const_to)
156 new_expr.
type()=type;
190 exprt &new_expr)
const 199 qual_from.
write(int_type);
201 if(expr.
type().
id()==ID_signedbv)
211 if(expr.
type().
id()==ID_unsignedbv)
218 int_type.
id(ID_unsignedbv);
223 if(expr.
type().
id()==ID_c_enum_tag)
242 exprt &new_expr)
const 298 exprt &new_expr)
const 300 if(type.
id()!=ID_signedbv &&
301 type.
id()!=ID_unsignedbv)
304 if(expr.
type().
id()!=ID_signedbv &&
305 expr.
type().
id()!=ID_unsignedbv &&
306 expr.
type().
id()!=ID_bool &&
307 expr.
type().
id()!=ID_c_enum_tag)
344 exprt &new_expr)
const 349 if(expr.
type().
id()==ID_floatbv ||
350 expr.
type().
id()==ID_fixedbv)
352 if(type.
id()!=ID_signedbv &&
353 type.
id()!=ID_unsignedbv)
356 else if(expr.
type().
id()==ID_signedbv ||
357 expr.
type().
id()==ID_unsignedbv ||
358 expr.
type().
id()==ID_c_enum_tag)
360 if(type.
id()!=ID_fixedbv &&
361 type.
id()!=ID_floatbv)
396 exprt &new_expr)
const 398 if(expr.
type().
id()!=ID_floatbv &&
399 expr.
type().
id()!=ID_fixedbv)
402 if(type.
id()!=ID_floatbv &&
403 type.
id()!=ID_fixedbv)
456 if(type.
id()!=ID_pointer ||
465 expr.
type().
id()!=ID_pointer)
468 new_expr.
set(ID_value, ID_NULL);
469 new_expr.
type()=type;
476 if(expr.
type().
id() != ID_pointer ||
484 if(sub_from.
id()==ID_nullptr)
488 if(sub_from.
id()!=ID_code && sub_to.id()==ID_empty)
499 if(sub_from.
id()==ID_struct && sub_to.id()==ID_struct)
552 if(type.
id()!=ID_pointer ||
557 if(expr.
type().
id() != ID_pointer ||
570 assert(this1.get(ID_C_base_name)==ID_this);
576 assert(this2.get(ID_C_base_name)==ID_this);
579 if(this2.type().subtype().get_bool(ID_C_constant) &&
580 !this1.type().subtype().get_bool(ID_C_constant))
594 if(expr.
id()==ID_constant &&
595 expr.
get(ID_value)==ID_NULL)
608 (type.
find(
"to-member"))));
635 if(expr.
type().
id()!=ID_signedbv &&
636 expr.
type().
id()!=ID_unsignedbv &&
637 expr.
type().
id()!=ID_pointer &&
638 expr.
type().
id()!=ID_c_enum_tag)
645 qual_from.
write(Bool);
680 exprt curr_expr=expr;
683 if(type.
id()==ID_c_bit_field)
687 if(curr_expr.type().id()==ID_c_bit_field)
688 curr_expr.make_typecast(curr_expr.type().subtype());
690 if(curr_expr.type().id()==ID_array)
692 if(type.
id()==ID_pointer)
698 else if(curr_expr.type().id()==ID_code &&
699 type.
id()==ID_pointer)
704 else if(curr_expr.get_bool(ID_C_lvalue))
712 curr_expr.
swap(new_expr);
716 if(
follow(type).
id()==ID_c_enum &&
717 follow(curr_expr.type()).
id()==ID_c_enum)
720 follow(curr_expr.type()).find(ID_tag))
732 curr_expr.type().
get(ID_C_c_type)!=type.
get(ID_C_c_type))
734 if(type.
id()==ID_signedbv ||
735 type.
id()==ID_unsignedbv ||
739 new_expr.
type() != type)
744 curr_expr, type, new_expr))
753 else if(type.
id()==ID_floatbv || type.
id()==ID_fixedbv)
756 new_expr.
type() != type)
759 curr_expr, type, new_expr) &&
761 curr_expr, type, new_expr))
769 else if(type.
id()==ID_pointer)
784 else if(type.
id()==ID_bool)
797 curr_expr.
swap(new_expr);
799 if(curr_expr.type().id()==ID_pointer)
801 typet sub_from=curr_expr.type();
807 sub_from.
swap(tmp_from);
812 qual_from.
read(sub_from);
815 qual_to.
read(sub_to);
817 if(qual_from!=qual_to)
823 while(sub_from.
id()==ID_pointer);
831 new_expr.
type()=type;
865 if(to.id()==ID_struct)
871 if(from.
id()==ID_struct)
884 if(expr.
id()==ID_dereference)
899 tmp_object_expr.set(ID_C_lvalue,
true);
901 new_expr.
swap(tmp_object_expr);
911 if(from.
id()==ID_struct)
918 for(struct_typet::componentst::const_iterator
923 const irept &component=*it;
925 if(component.
get_bool(ID_from_base))
928 if(component.
get_bool(
"is_explicit"))
931 const typet &comp_type =
932 static_cast<const typet&
>(component.
find(ID_type));
934 if(comp_type.
id() !=ID_code)
937 if(comp_type.
find(ID_return_type).
id() !=ID_constructor)
942 const irept ¶meters=comp_type.
find(ID_parameters);
944 if(parameters.
get_sub().size() != 2)
960 if(tmp.
id()==ID_struct)
969 expr, arg1_type, tmp_expr, tmp_rank))
977 tmp_expr.
set(ID_C_lvalue,
true);
982 func_symb.
type()=comp_type;
984 exprt tmp(
"already_typechecked");
986 func_symb.
swap(func_symb);
993 ctor_expr.
arguments().push_back(tmp_expr);
996 new_expr.
swap(ctor_expr);
997 assert(new_expr.
get(ID_statement)==ID_temporary_object);
999 if(to.get_bool(ID_C_constant))
1000 new_expr.
type().
set(ID_C_constant,
true);
1014 expr_pfrom, pto, expr_ptmp, tmp_rank))
1025 expr_deref.
set(ID_C_lvalue,
true);
1028 exprt new_object(
"new_object", type);
1029 new_object.
set(ID_C_lvalue,
true);
1030 new_object.
type().
set(ID_C_constant,
false);
1033 func_symb.
type()=comp_type;
1035 exprt tmp(
"already_typechecked");
1037 func_symb.
swap(func_symb);
1043 ctor_expr.
arguments().push_back(expr_deref);
1046 new_expr.
swap(ctor_expr);
1049 new_expr.
get(ID_statement)==ID_temporary_object,
1052 if(to.get_bool(ID_C_constant))
1053 new_expr.
type().
set(ID_C_constant,
true);
1063 if(from.
id()==ID_struct)
1068 for(struct_typet::componentst::const_iterator
1072 const irept &component=*it;
1073 const typet comp_type=
static_cast<const typet&
>(component.
find(ID_type));
1075 if(component.
get_bool(ID_from_base))
1078 if(!component.
get_bool(
"is_cast_operator"))
1081 assert(component.
get(ID_type)==ID_code &&
1085 static_cast<const typet&
>(comp_type.
find(ID_parameters)
1089 this_type.
set(ID_C_reference,
true);
1091 exprt this_expr(expr);
1092 this_type.set(ID_C_this,
true);
1094 unsigned tmp_rank=0;
1098 this_expr, this_type, tmp_expr, tmp_rank))
1102 irept func_name(ID_name);
1103 func_name.
set(ID_identifier, component.
get(ID_base_name));
1105 cpp_func_name.
get_sub().push_back(func_name);
1107 exprt member_func(ID_member);
1108 member_func.
add(ID_component_cpp_name)=cpp_func_name;
1109 exprt ac(
"already_typechecked");
1127 new_expr.
swap(tmp_expr);
1144 const typet &type)
const 1153 if(from.
get(ID_C_c_type)!=to.get(ID_C_c_type))
1159 if(from.
id()==ID_struct &&
1164 if(from.
id()==ID_struct &&
1182 unsigned &rank)
const 1199 if(qual_from!=qual_to)
1251 unsigned backup_rank=rank;
1257 if(expr.
get(ID_statement)==ID_temporary_object)
1258 expr.
set(ID_C_lvalue,
true);
1259 else if(expr.
get(ID_statement)==ID_function_call)
1260 expr.
set(ID_C_lvalue,
true);
1261 else if(expr.
get_bool(ID_C_temporary_avoided))
1263 expr.
remove(ID_C_temporary_avoided);
1266 expr.
swap(temporary);
1267 expr.
set(ID_C_lvalue,
true);
1303 for(struct_typet::componentst::const_iterator
1307 const irept &component=*it;
1309 if(component.
get_bool(ID_from_base))
1312 if(!component.
get_bool(
"is_cast_operator"))
1322 assert(component_type.
parameters().size()==1);
1326 this_type.set(ID_C_reference,
true);
1328 exprt this_expr(expr);
1330 this_type.set(ID_C_this,
true);
1332 unsigned tmp_rank=0;
1336 this_expr, this_type, tmp_expr, tmp_rank))
1340 irept func_name(ID_name);
1341 func_name.
set(ID_identifier, component.
get(ID_base_name));
1343 cpp_func_name.
get_sub().push_back(func_name);
1345 exprt member_func(ID_member);
1346 member_func.
add(ID_component_cpp_name)=cpp_func_name;
1347 exprt ac(
"already_typechecked");
1357 exprt returned_value=func_expr;
1360 if(returned_value.
get_bool(ID_C_lvalue) &&
1364 assert(returned_value.
id()==ID_dereference &&
1367 new_expr=returned_value.
op0();
1372 qual_from.
read(returned_value.
type());
1396 exprt arg_expr=expr;
1401 arg_expr.
set(ID_C_lvalue,
true);
1418 tmp.
set(ID_statement, ID_temporary_object);
1426 tmp.
type().
set(ID_C_reference,
true);
1448 unsigned backup_rank=rank;
1461 new_expr.
type().
set(ID_C_reference,
true);
1522 error() <<
"invalid implicit conversion from `" 1526 str <<
"\n " <<
follow(e.
type()).pretty() <<
'\n';
1527 str <<
"\n " << type.
pretty() <<
'\n';
1586 expr.
swap(new_expr);
1591 error() <<
"bad reference initializer" <<
eom;
1597 const typet &t2)
const 1599 assert(t1.
id()==ID_pointer && t2.
id()==ID_pointer);
1604 nt1.
remove(ID_C_reference);
1605 nt1.remove(
"to-member");
1608 nt2.
remove(ID_C_reference);
1612 std::vector<typet> snt1;
1613 snt1.push_back(nt1);
1615 while(snt1.back().has_subtype())
1617 snt1.reserve(snt1.size()+1);
1618 snt1.push_back(snt1.back().subtype());
1622 q1.
read(snt1.back());
1628 std::vector<typet> snt2;
1629 snt2.push_back(nt2);
1630 while(snt2.back().has_subtype())
1632 snt2.reserve(snt2.size()+1);
1633 snt2.push_back(snt2.back().subtype());
1637 q2.
read(snt2.back());
1643 const std::size_t k=snt1.size() < snt2.size() ? snt1.size() : snt2.size();
1645 for(std::size_t i=k; i > 1; i--)
1647 snt1[snt1.size()-2].subtype()=snt1[snt1.size()-1];
1650 snt2[snt2.size()-2].subtype()=snt2[snt2.size()-1];
1654 exprt e1(
"Dummy", snt1.back());
1667 exprt curr_expr=expr;
1669 if(curr_expr.
type().
id()==ID_array)
1671 if(type.
id()==ID_pointer)
1677 else if(curr_expr.
type().
id()==ID_code &&
1678 type.
id()==ID_pointer)
1683 else if(curr_expr.
get_bool(ID_C_lvalue))
1701 new_expr=address_of;
1704 else if(type.
id()==ID_pointer)
1706 if(type!=new_expr.
type())
1711 new_expr.
swap(typecast_expr);
1725 if(type.
id()==ID_pointer)
1727 if(e.
id()==ID_dereference && e.
get_bool(ID_C_implicit))
1730 if(e.
type().
id()==ID_pointer &&
1742 else if(type.
id()==ID_pointer)
1774 bool check_constantness)
1778 if(check_constantness && type.
id()==ID_pointer)
1780 if(e.
id()==ID_dereference && e.
get_bool(ID_C_implicit))
1783 if(e.
type().
id()==ID_pointer &&
1802 if(e.
type().
id()==ID_array)
1819 if(e.
type().
id()==ID_pointer &&
1820 (type.
id()==ID_unsignedbv || type.
id()==ID_signedbv))
1828 if((e.
type().
id()==ID_unsignedbv ||
1829 e.
type().
id()==ID_signedbv ||
1830 e.
type().
id()==ID_bool) &&
1831 type.
id()==ID_pointer &&
1839 new_expr.
set(ID_value, ID_NULL);
1840 new_expr.
type()=type;
1850 if(e.
type().
id()==ID_pointer &&
1851 type.
id()==ID_pointer &&
1876 bool check_constantness)
1880 if(check_constantness && type.
id()==ID_pointer)
1882 if(e.
id()==ID_dereference && e.
get_bool(ID_C_implicit))
1885 if(e.
type().
id()==ID_pointer &&
1901 if(subto.
id()==ID_struct && from.id()==ID_struct)
1920 if(e.
id()==ID_dereference)
1929 new_expr.
swap(address_of);
1936 if(type.
id()==ID_empty)
1944 if(type.
id()==ID_c_enum_tag &&
1945 (e.
type().
id()==ID_signedbv ||
1946 e.
type().
id()==ID_unsignedbv ||
1947 e.
type().
id()==ID_c_enum_tag))
1951 new_expr.
remove(ID_C_lvalue);
1959 exprt tc(ID_already_typechecked);
1963 new_expr.
swap(temporary);
1968 new_expr.
set(ID_C_temporary_avoided,
true);
1970 new_expr.
remove(ID_C_lvalue);
1976 if(type.
id()==ID_pointer && e.
type().
id()==ID_pointer)
1984 if(from.id()==ID_empty)
1991 if(to.
id()==ID_struct && from.id()==ID_struct)
2024 follow(static_cast<const typet&>(type.
find(
"to-member"))));
2044 new_expr.
type().
add(
"to-member") = from_struct;
The type of an expression.
struct configt::ansi_ct ansi_c
void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
bool reference_binding(exprt expr, const typet &type, exprt &new_expr, unsigned &rank)
Reference binding.
pointer_typet pointer_type(const typet &subtype)
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
bool standard_conversion_floating_point_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-point conversion.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
void add_implicit_dereference(exprt &expr)
bool static_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
bool standard_conversion_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Integral conversion.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void copy_to_operands(const exprt &expr)
bool user_defined_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
User-defined conversion sequence.
void move_to_operands(exprt &expr)
bool standard_conversion_qualification(const exprt &expr, const typet &, exprt &new_expr) const
Qualification conversion.
bool standard_conversion_floating_point_promotion(const exprt &expr, exprt &new_expr) const
Floating-point-promotion conversion.
void show_instantiation_stack(std::ostream &)
const componentst & components() const
bitvector_typet double_type()
virtual void implicit_typecast(exprt &expr, const typet &type)
static mstreamt & eom(mstreamt &m)
bool standard_conversion_function_to_pointer(const exprt &expr, exprt &new_expr) const
Function-to-pointer conversion.
bool get_bool(const irep_namet &name) const
bool cast_away_constness(const typet &t1, const typet &t2) const
bool standard_conversion_integral_promotion(const exprt &expr, exprt &new_expr) const
Integral-promotion conversion.
#define INVARIANT(CONDITION, REASON)
bool reference_compatible(const exprt &expr, const typet &type, unsigned &rank) const
Reference-compatible.
bool dynamic_typecast(const exprt &expr, const typet &type, exprt &new_expr)
bool standard_conversion_floating_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-integral conversion.
bool reference_related(const exprt &expr, const typet &type) const
Reference-related.
const irep_idt & id() const
bitvector_typet float_type()
reference_typet reference_type(const typet &subtype)
const source_locationt & find_source_location() const
source_locationt source_location
bool cpp_is_pod(const typet &type) const
Operator to dereference a pointer.
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
API to expression classes.
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
const irep_idt & get(const irep_namet &name) const
virtual void read(const typet &src) override
Base class for tree-like data structures with sharing.
bool standard_conversion_pointer_to_member(const exprt &expr, const typet &type, exprt &new_expr)
Pointer-to-member conversion.
C++ Language Type Checking.
const typet & follow(const typet &) const
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Operator to return the address of an object.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void make_ptr_typecast(exprt &expr, const typet &dest_type)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
A function call side effect.
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
bool standard_conversion_lvalue_to_rvalue(const exprt &expr, exprt &new_expr) const
Lvalue-to-rvalue conversion.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
virtual bool is_subset_of(const qualifierst &other) const override
bool standard_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
Standard Conversion Sequence.
Base class for all expressions.
const parameterst & parameters() const
const source_locationt & source_location() const
irept & add(const irep_namet &name)
virtual std::string to_string(const typet &type)
exprt::operandst & arguments()
virtual void write(typet &src) const override
source_locationt & add_source_location()
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
bool standard_conversion_pointer(const exprt &expr, const typet &type, exprt &new_expr)
Pointer conversion.
signedbv_typet signed_int_type()
exprt cpp_symbol_expr(const symbolt &symbol)
void remove(const irep_namet &name)
const typet & subtype() const
An expression containing a side effect.
bool implicit_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
implicit conversion sequence
void make_typecast(const typet &_type)
const irept & find(const irep_namet &name) const
const typet & return_type() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)
void reference_initializer(exprt &expr, const typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows: ...
bool standard_conversion_boolean(const exprt &expr, exprt &new_expr) const
Boolean conversion.
bool simplify(exprt &expr, const namespacet &ns)