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)
893 exprt deref(ID_dereference);
898 exprt tmp_object_expr=
exprt(ID_side_effect, type);
899 tmp_object_expr.
set(ID_statement, ID_temporary_object);
902 tmp_object_expr.
set(ID_C_lvalue,
true);
904 new_expr.
swap(tmp_object_expr);
914 if(from.
id()==ID_struct)
921 for(struct_typet::componentst::const_iterator
926 const irept &component=*it;
928 if(component.
get_bool(ID_from_base))
931 if(component.
get_bool(
"is_explicit"))
934 const typet &comp_type =
935 static_cast<const typet&
>(component.
find(ID_type));
937 if(comp_type.
id() !=ID_code)
940 if(comp_type.
find(ID_return_type).
id() !=ID_constructor)
945 const irept ¶meters=comp_type.
find(ID_parameters);
947 if(parameters.
get_sub().size() != 2)
963 if(tmp.
id()==ID_struct)
972 expr, arg1_type, tmp_expr, tmp_rank))
980 tmp_expr.
set(ID_C_lvalue,
true);
985 func_symb.
type()=comp_type;
987 exprt tmp(
"already_typechecked");
989 func_symb.
swap(func_symb);
996 ctor_expr.
arguments().push_back(tmp_expr);
999 new_expr.
swap(ctor_expr);
1000 assert(new_expr.
get(ID_statement)==ID_temporary_object);
1002 if(to.get_bool(ID_C_constant))
1003 new_expr.
type().
set(ID_C_constant,
true);
1017 expr_pfrom, pto, expr_ptmp, tmp_rank))
1029 expr_deref.
set(ID_C_lvalue,
true);
1033 exprt new_object(
"new_object", type);
1034 new_object.
set(ID_C_lvalue,
true);
1035 new_object.
type().
set(ID_C_constant,
false);
1038 func_symb.
type()=comp_type;
1040 exprt tmp(
"already_typechecked");
1042 func_symb.
swap(func_symb);
1048 ctor_expr.
arguments().push_back(expr_deref);
1051 new_expr.
swap(ctor_expr);
1054 new_expr.
get(ID_statement)==ID_temporary_object,
1057 if(to.get_bool(ID_C_constant))
1058 new_expr.
type().
set(ID_C_constant,
true);
1068 if(from.
id()==ID_struct)
1073 for(struct_typet::componentst::const_iterator
1077 const irept &component=*it;
1078 const typet comp_type=
static_cast<const typet&
>(component.
find(ID_type));
1080 if(component.
get_bool(ID_from_base))
1083 if(!component.
get_bool(
"is_cast_operator"))
1086 assert(component.
get(ID_type)==ID_code &&
1090 static_cast<const typet&
>(comp_type.
find(ID_parameters)
1094 this_type.
set(ID_C_reference,
true);
1096 exprt this_expr(expr);
1097 this_type.set(ID_C_this,
true);
1099 unsigned tmp_rank=0;
1103 this_expr, this_type, tmp_expr, tmp_rank))
1107 irept func_name(ID_name);
1108 func_name.
set(ID_identifier, component.
get(ID_base_name));
1110 cpp_func_name.
get_sub().push_back(func_name);
1112 exprt member_func(ID_member);
1113 member_func.
add(ID_component_cpp_name)=cpp_func_name;
1114 exprt ac(
"already_typechecked");
1132 new_expr.
swap(tmp_expr);
1149 const typet &type)
const 1158 if(from.
get(ID_C_c_type)!=to.get(ID_C_c_type))
1164 if(from.
id()==ID_struct &&
1169 if(from.
id()==ID_struct &&
1187 unsigned &rank)
const 1204 if(qual_from!=qual_to)
1256 unsigned backup_rank=rank;
1262 if(expr.
get(ID_statement)==ID_temporary_object)
1263 expr.
set(ID_C_lvalue,
true);
1264 else if(expr.
get(ID_statement)==ID_function_call)
1265 expr.
set(ID_C_lvalue,
true);
1266 else if(expr.
get_bool(
"#temporary_avoided"))
1268 expr.
remove(
"#temporary_avoided");
1271 expr.
swap(temporary);
1272 expr.
set(ID_C_lvalue,
true);
1287 tmp.
type().
set(ID_C_reference,
true);
1311 for(struct_typet::componentst::const_iterator
1315 const irept &component=*it;
1317 if(component.
get_bool(ID_from_base))
1320 if(!component.
get_bool(
"is_cast_operator"))
1330 assert(component_type.
parameters().size()==1);
1334 this_type.set(ID_C_reference,
true);
1336 exprt this_expr(expr);
1338 this_type.set(ID_C_this,
true);
1340 unsigned tmp_rank=0;
1344 this_expr, this_type, tmp_expr, tmp_rank))
1348 irept func_name(ID_name);
1349 func_name.
set(ID_identifier, component.
get(ID_base_name));
1351 cpp_func_name.
get_sub().push_back(func_name);
1353 exprt member_func(ID_member);
1354 member_func.
add(ID_component_cpp_name)=cpp_func_name;
1355 exprt ac(
"already_typechecked");
1365 exprt returned_value=func_expr;
1368 if(returned_value.
get_bool(ID_C_lvalue) &&
1372 assert(returned_value.
id()==ID_dereference &&
1375 new_expr=returned_value.
op0();
1380 qual_from.
read(returned_value.
type());
1404 exprt arg_expr=expr;
1409 arg_expr.
set(ID_C_lvalue,
true);
1417 tmp.
type().
set(ID_C_reference,
true);
1429 tmp.
set(ID_statement, ID_temporary_object);
1437 tmp.
type().
set(ID_C_reference,
true);
1459 unsigned backup_rank=rank;
1472 new_expr.
type().
set(ID_C_reference,
true);
1526 error() <<
"invalid implicit conversion from `" 1530 str <<
"\n " <<
follow(e.
type()).pretty() <<
'\n';
1531 str <<
"\n " << type.
pretty() <<
'\n';
1590 expr.
swap(new_expr);
1595 error() <<
"bad reference initializer" <<
eom;
1601 const typet &t2)
const 1603 assert(t1.
id()==ID_pointer && t2.
id()==ID_pointer);
1608 nt1.
remove(ID_C_reference);
1611 nt2.
remove(ID_C_reference);
1614 std::vector<typet> snt1;
1615 snt1.push_back(nt1);
1617 while(snt1.back().has_subtype())
1619 snt1.reserve(snt1.size()+1);
1620 snt1.push_back(snt1.back().subtype());
1624 q1.
read(snt1.back());
1630 std::vector<typet> snt2;
1631 snt2.push_back(nt2);
1632 while(snt2.back().has_subtype())
1634 snt2.reserve(snt2.size()+1);
1635 snt2.push_back(snt2.back().subtype());
1639 q2.
read(snt2.back());
1645 const std::size_t k=snt1.size() < snt2.size() ? snt1.size() : snt2.size();
1647 for(std::size_t i=k; i > 1; i--)
1649 snt1[snt1.size()-2].subtype()=snt1[snt1.size()-1];
1652 snt2[snt2.size()-2].subtype()=snt2[snt2.size()-1];
1656 exprt e1(
"Dummy", snt1.back());
1669 exprt curr_expr=expr;
1671 if(curr_expr.
type().
id()==ID_array)
1673 if(type.
id()==ID_pointer)
1679 else if(curr_expr.
type().
id()==ID_code &&
1680 type.
id()==ID_pointer)
1685 else if(curr_expr.
get_bool(ID_C_lvalue))
1703 new_expr=address_of;
1706 else if(type.
id()==ID_pointer)
1708 if(type!=new_expr.
type())
1713 new_expr.
swap(typecast_expr);
1727 if(type.
id()==ID_pointer)
1729 if(e.
id()==ID_dereference && e.
get_bool(ID_C_implicit))
1732 if(e.
type().
id()==ID_pointer &&
1744 else if(type.
id()==ID_pointer)
1776 bool check_constantness)
1780 if(check_constantness && type.
id()==ID_pointer)
1782 if(e.
id()==ID_dereference && e.
get_bool(ID_C_implicit))
1785 if(e.
type().
id()==ID_pointer &&
1804 if(e.
type().
id()==ID_array)
1821 if(e.
type().
id()==ID_pointer &&
1822 (type.
id()==ID_unsignedbv || type.
id()==ID_signedbv))
1830 if((e.
type().
id()==ID_unsignedbv ||
1831 e.
type().
id()==ID_signedbv ||
1832 e.
type().
id()==ID_bool) &&
1833 type.
id()==ID_pointer &&
1841 new_expr.
set(ID_value, ID_NULL);
1842 new_expr.
type()=type;
1852 if(e.
type().
id()==ID_pointer &&
1853 type.
id()==ID_pointer &&
1878 bool check_constantness)
1882 if(check_constantness && type.
id()==ID_pointer)
1884 if(e.
id()==ID_dereference && e.
get_bool(ID_C_implicit))
1887 if(e.
type().
id()==ID_pointer &&
1903 if(subto.
id()==ID_struct && from.id()==ID_struct)
1922 if(e.
id()==ID_dereference)
1931 new_expr.
swap(address_of);
1938 if(type.
id()==ID_empty)
1946 if(type.
id()==ID_c_enum_tag &&
1947 (e.
type().
id()==ID_signedbv ||
1948 e.
type().
id()==ID_unsignedbv ||
1949 e.
type().
id()==ID_c_enum_tag))
1953 new_expr.
remove(ID_C_lvalue);
1961 exprt tc(ID_already_typechecked);
1965 new_expr.
swap(temporary);
1970 new_expr.
set(
"#temporary_avoided",
true);
1972 new_expr.
remove(ID_C_lvalue);
1978 if(type.
id()==ID_pointer && e.
type().
id()==ID_pointer)
1986 if(from.id()==ID_empty)
1993 if(to.
id()==ID_struct && from.id()==ID_struct)
2026 follow(static_cast<const typet&>(type.
find(
"to-member"))));
The type of an expression.
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
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.
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.
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.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
#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.
void read(const typet &src)
bool reference_related(const exprt &expr, const typet &type) const
Reference-related.
const irep_idt & id() const
bitvector_typet float_type()
const source_locationt & find_source_location() const
source_locationt source_location
bool cpp_is_pod(const typet &type) const
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
void write(typet &src) const
API to expression classes.
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
const irep_idt & get(const irep_namet &name) const
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.
bitvector_typet index_type()
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_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 struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
A function call side effect.
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
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.
bool is_subset_of(const c_qualifierst &q) const
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 signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
const source_locationt & source_location() const
irept & add(const irep_namet &name)
virtual std::string to_string(const typet &type)
exprt::operandst & arguments()
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
source_locationt & add_source_location()
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
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
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
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)