Go to the documentation of this file.
49 exprt &new_expr)
const
53 if(expr.
type().
id() == ID_code)
57 expr.
type().
id() == ID_struct &&
65 new_expr.
remove(ID_C_lvalue);
80 exprt &new_expr)
const
82 assert(expr.
type().
id()==ID_array);
88 index.
set(ID_C_lvalue,
true);
121 exprt &new_expr)
const
123 if(expr.
type().
id()!=ID_pointer ||
130 if(expr.
type()!=type)
137 while(sub_from.
id()==ID_pointer)
148 if(qual_from!=qual_to && !const_to)
164 new_expr.
type()=type;
198 exprt &new_expr)
const
207 qual_from.
write(int_type);
209 if(expr.
type().
id()==ID_signedbv)
218 if(expr.
type().
id()==ID_unsignedbv)
227 if(expr.
type().
id() == ID_bool || expr.
type().
id() == ID_c_bool)
233 if(expr.
type().
id()==ID_c_enum_tag)
251 exprt &new_expr)
const
306 exprt &new_expr)
const
308 if(type.
id()!=ID_signedbv &&
309 type.
id()!=ID_unsignedbv)
313 expr.
type().
id() != ID_signedbv && expr.
type().
id() != ID_unsignedbv &&
314 expr.
type().
id() != ID_c_bool && expr.
type().
id() != ID_bool &&
315 expr.
type().
id() != ID_c_enum_tag)
353 exprt &new_expr)
const
358 if(expr.
type().
id()==ID_floatbv ||
359 expr.
type().
id()==ID_fixedbv)
361 if(type.
id()!=ID_signedbv &&
362 type.
id()!=ID_unsignedbv)
365 else if(expr.
type().
id()==ID_signedbv ||
366 expr.
type().
id()==ID_unsignedbv ||
367 expr.
type().
id()==ID_c_enum_tag)
369 if(type.
id()!=ID_fixedbv &&
370 type.
id()!=ID_floatbv)
404 exprt &new_expr)
const
406 if(expr.
type().
id()!=ID_floatbv &&
407 expr.
type().
id()!=ID_fixedbv)
410 if(type.
id()!=ID_floatbv &&
411 type.
id()!=ID_fixedbv)
463 if(type.
id()!=ID_pointer ||
472 expr.
type().
id()!=ID_pointer)
475 new_expr.
set(ID_value, ID_NULL);
476 new_expr.
type()=type;
484 expr.
type().
id() != ID_pointer ||
494 if(sub_from.
id()==ID_nullptr)
498 if(sub_from.
id()!=ID_code && sub_to.
id()==ID_empty)
508 if(sub_from.
id()==ID_struct && sub_to.
id()==ID_struct)
604 if(expr.
id()==ID_constant &&
605 expr.
get(ID_value)==ID_NULL)
642 expr.
type().
id() != ID_signedbv && expr.
type().
id() != ID_unsignedbv &&
643 expr.
type().
id() != ID_pointer && expr.
type().
id() != ID_bool &&
644 expr.
type().
id() != ID_c_enum_tag)
653 qual_from.
write(Bool);
687 exprt curr_expr=expr;
690 if(type.
id()==ID_c_bit_field)
694 if(curr_expr.
type().
id()==ID_c_bit_field)
697 if(curr_expr.
type().
id()==ID_array)
699 if(type.
id()==ID_pointer)
705 else if(curr_expr.
type().
id()==ID_code &&
706 type.
id()==ID_pointer)
711 else if(curr_expr.
get_bool(ID_C_lvalue))
719 curr_expr.
swap(new_expr);
723 if(
follow(type).
id()==ID_c_enum &&
726 if(
follow(type).find(ID_tag)==
739 curr_expr.
type().
get(ID_C_c_type)!=type.
get(ID_C_c_type))
741 if(type.
id()==ID_signedbv ||
742 type.
id()==ID_unsignedbv ||
743 follow(type).
id()==ID_c_enum)
746 new_expr.
type() != type)
751 curr_expr, type, new_expr))
760 else if(type.
id()==ID_floatbv || type.
id()==ID_fixedbv)
763 new_expr.
type() != type)
766 curr_expr, type, new_expr) &&
768 curr_expr, type, new_expr))
776 else if(type.
id()==ID_pointer)
791 else if(type.
id() == ID_c_bool)
798 else if(type.
id() == ID_bool)
810 curr_expr.
swap(new_expr);
812 if(curr_expr.
type().
id()==ID_pointer)
820 sub_from.
swap(tmp_from);
825 qual_from.
read(sub_from);
828 qual_to.
read(sub_to);
830 if(qual_from!=qual_to)
836 while(sub_from.
id()==ID_pointer);
844 new_expr.
type()=type;
878 if(to.
id()==ID_struct)
884 if(from.
id()==ID_struct)
897 if(expr.
id()==ID_dereference)
912 tmp_object_expr.
set(ID_C_lvalue,
true);
913 tmp_object_expr.
set(ID_mode, ID_cpp);
915 new_expr.
swap(tmp_object_expr);
934 if(comp_type.
id() !=ID_code)
944 if(parameters.size() != 2)
947 exprt curr_arg1 = parameters[1];
957 if(arg1_type.
id() != ID_struct_tag)
961 expr, arg1_type, tmp_expr, tmp_rank))
969 tmp_expr.
set(ID_C_lvalue,
true);
974 func_symb.
type()=comp_type;
979 std::move(func_symb),
985 new_expr.
swap(ctor_expr);
986 assert(new_expr.
get(ID_statement)==ID_temporary_object);
989 new_expr.
type().
set(ID_C_constant,
true);
994 else if(from.
id() == ID_struct && arg1_type.
id() == ID_struct_tag)
1003 expr_pfrom, pto, expr_ptmp, tmp_rank))
1014 expr_deref.
set(ID_C_lvalue,
true);
1017 exprt new_object(ID_new_object, type);
1018 new_object.
set(ID_C_lvalue,
true);
1019 new_object.
type().
set(ID_C_constant,
false);
1022 func_symb.
type()=comp_type;
1026 std::move(func_symb),
1032 new_expr.
swap(ctor_expr);
1035 new_expr.
get(ID_statement)==ID_temporary_object,
1039 new_expr.
type().
set(ID_C_constant,
true);
1049 if(from.
id()==ID_struct)
1057 if(!
component.get_bool(ID_is_cast_operator))
1062 comp_type.
parameters().size() == 1,
"expected exactly one parameter");
1065 this_type.
set(ID_C_reference,
true);
1067 exprt this_expr(expr);
1068 this_type.
set(ID_C_this,
true);
1070 unsigned tmp_rank=0;
1074 this_expr, this_type, tmp_expr, tmp_rank))
1080 exprt member_func(ID_member);
1081 member_func.
add(ID_component_cpp_name)=cpp_func_name;
1085 std::move(member_func),
1099 new_expr.
swap(tmp_expr);
1116 const typet &type)
const
1125 if(from.
get(ID_C_c_type)!=to.
get(ID_C_c_type))
1131 if(from.
id()==ID_struct &&
1136 if(from.
id()==ID_struct &&
1154 unsigned &rank)
const
1171 if(qual_from!=qual_to)
1223 unsigned backup_rank=rank;
1229 if(expr.
get(ID_statement)==ID_temporary_object)
1230 expr.
set(ID_C_lvalue,
true);
1231 else if(expr.
get(ID_statement)==ID_function_call)
1232 expr.
set(ID_C_lvalue,
true);
1233 else if(expr.
get_bool(ID_C_temporary_avoided))
1235 expr.
remove(ID_C_temporary_avoided);
1238 expr.
swap(temporary);
1239 expr.
set(ID_C_lvalue,
true);
1256 tmp.
set(ID_mode, ID_cpp);
1289 if(!
component.get_bool(ID_is_cast_operator))
1298 assert(component_type.
parameters().size()==1);
1302 this_type.
set(ID_C_reference,
true);
1304 exprt this_expr(expr);
1306 this_type.
set(ID_C_this,
true);
1308 unsigned tmp_rank=0;
1312 this_expr, this_type, tmp_expr, tmp_rank))
1318 exprt member_func(ID_member);
1319 member_func.
add(ID_component_cpp_name)=cpp_func_name;
1323 std::move(member_func),
1330 exprt returned_value=func_expr;
1333 if(returned_value.
get_bool(ID_C_lvalue) &&
1339 "the returned value must be pointer to reference");
1346 qual_from.
read(returned_value.
type());
1370 exprt arg_expr=expr;
1372 if(arg_expr.
type().
id() == ID_struct_tag)
1375 arg_expr.
set(ID_C_lvalue,
true);
1393 tmp.
set(ID_mode, ID_cpp);
1400 tmp.
type().
set(ID_C_reference,
true);
1422 unsigned backup_rank=rank;
1435 new_expr.
type().
set(ID_C_reference,
true);
1500 str <<
"\n " << type.
pretty() <<
'\n';
1559 expr.
swap(new_expr);
1564 error() <<
"bad reference initializer" <<
eom;
1570 const typet &t2)
const
1572 assert(t1.
id()==ID_pointer && t2.
id()==ID_pointer);
1577 nt1.
remove(ID_C_reference);
1578 nt1.
remove(ID_to_member);
1581 nt2.
remove(ID_C_reference);
1582 nt2.
remove(ID_to_member);
1585 std::vector<typet> snt1;
1586 snt1.push_back(nt1);
1588 while(snt1.back().has_subtype())
1590 snt1.reserve(snt1.size()+1);
1591 snt1.push_back(snt1.back().subtype());
1595 q1.
read(snt1.back());
1601 std::vector<typet> snt2;
1602 snt2.push_back(nt2);
1603 while(snt2.back().has_subtype())
1605 snt2.reserve(snt2.size()+1);
1606 snt2.push_back(snt2.back().subtype());
1610 q2.
read(snt2.back());
1616 const std::size_t k=snt1.size() < snt2.size() ? snt1.size() : snt2.size();
1618 for(std::size_t i=k; i > 1; i--)
1620 snt1[snt1.size()-2].subtype()=snt1[snt1.size()-1];
1623 snt2[snt2.size()-2].subtype()=snt2[snt2.size()-1];
1627 exprt e1(
"Dummy", snt1.back());
1640 exprt curr_expr=expr;
1642 if(curr_expr.
type().
id()==ID_array)
1644 if(type.
id()==ID_pointer)
1650 else if(curr_expr.
type().
id()==ID_code &&
1651 type.
id()==ID_pointer)
1656 else if(curr_expr.
get_bool(ID_C_lvalue))
1674 new_expr=address_of;
1677 else if(type.
id()==ID_pointer)
1679 if(type!=new_expr.
type())
1684 new_expr.
swap(typecast_expr);
1698 if(type.
id()==ID_pointer)
1700 if(e.
id()==ID_dereference && e.
get_bool(ID_C_implicit))
1703 if(e.
type().
id()==ID_pointer &&
1712 if(type.
subtype().
id() != ID_struct_tag)
1715 else if(type.
id()==ID_pointer)
1726 else if(type.
subtype().
id() == ID_struct_tag)
1747 bool check_constantness)
1751 if(check_constantness && type.
id()==ID_pointer)
1753 if(e.
id()==ID_dereference && e.
get_bool(ID_C_implicit))
1756 if(e.
type().
id()==ID_pointer &&
1775 if(e.
type().
id()==ID_array)
1792 if(e.
type().
id()==ID_pointer &&
1793 (type.
id()==ID_unsignedbv || type.
id()==ID_signedbv))
1801 (e.
type().
id() == ID_unsignedbv || e.
type().
id() == ID_signedbv ||
1802 e.
type().
id() == ID_c_bool || e.
type().
id() == ID_bool) &&
1810 new_expr.
set(ID_value, ID_NULL);
1811 new_expr.
type()=type;
1820 if(e.
type().
id()==ID_pointer &&
1821 type.
id()==ID_pointer &&
1843 bool check_constantness)
1847 if(check_constantness && type.
id()==ID_pointer)
1849 if(e.
id()==ID_dereference && e.
get_bool(ID_C_implicit))
1852 if(e.
type().
id()==ID_pointer &&
1868 if(subto.
id()==ID_struct && from.
id()==ID_struct)
1887 if(e.
id()==ID_dereference)
1896 new_expr.
swap(address_of);
1903 if(type.
id()==ID_empty)
1910 if(type.
id()==ID_c_enum_tag &&
1911 (e.
type().
id()==ID_signedbv ||
1912 e.
type().
id()==ID_unsignedbv ||
1913 e.
type().
id()==ID_c_enum_tag))
1916 new_expr.
remove(ID_C_lvalue);
1930 new_expr.
swap(temporary);
1935 new_expr.
set(ID_C_temporary_avoided,
true);
1937 new_expr.
remove(ID_C_lvalue);
1943 if(type.
id()==ID_pointer && e.
type().
id()==ID_pointer)
1950 if(from.
id()==ID_empty)
1956 if(to.
id()==ID_struct && from.
id()==ID_struct)
2007 new_expr.
type().
add(ID_to_member) = from_struct;
virtual void read(const typet &src) override
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
#define UNREACHABLE
This should be used to mark dead code.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
static exprt conditional_cast(const exprt &expr, const typet &type)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const typet & subtype() const
bool standard_conversion_floating_point_promotion(const exprt &expr, exprt &new_expr) const
Floating-point-promotion conversion.
bool standard_conversion_boolean(const exprt &expr, exprt &new_expr) const
Boolean conversion.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool reference_binding(exprt expr, const typet &type, exprt &new_expr, unsigned &rank)
Reference binding.
The type of an expression, extends irept.
void show_instantiation_stack(std::ostream &)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
bool reinterpret_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
Operator to dereference a pointer.
A side_effect_exprt representation of a function call side effect.
bool standard_conversion_integral_promotion(const exprt &expr, exprt &new_expr) const
Integral-promotion conversion.
irept & add(const irep_namet &name)
const irept & find(const irep_namet &name) const
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
bool standard_conversion_lvalue_to_rvalue(const exprt &expr, exprt &new_expr) const
Lvalue-to-rvalue conversion.
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
bool standard_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
Standard Conversion Sequence.
Base class for all expressions.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
bool reference_compatible(const exprt &expr, const typet &type, unsigned &rank) const
Reference-compatible.
struct configt::ansi_ct ansi_c
virtual bool is_subset_of(const qualifierst &other) const override
bitvector_typet index_type()
bool standard_conversion_array_to_pointer(const exprt &expr, exprt &new_expr) const
Array-to-pointer conversion.
bool cpp_is_pod(const typet &type) const
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
bool standard_conversion_floating_point_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-point conversion.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
signedbv_typet signed_int_type()
static void make_already_typechecked(exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
void add_implicit_dereference(exprt &)
source_locationt source_location
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:
#define PRECONDITION(CONDITION)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
virtual void write(typet &src) const override
floatbv_typet float_type()
API to expression classes for Pointers.
bool simplify(exprt &expr, const namespacet &ns)
void make_ptr_typecast(exprt &expr, const typet &dest_type)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt simplify_expr(exprt src, const namespacet &ns)
pointer_typet pointer_type(const typet &subtype)
bool subtype_typecast(const struct_typet &from, const struct_typet &to) const
const irep_idt & id() const
bool standard_conversion_function_to_pointer(const exprt &expr, exprt &new_expr) const
Function-to-pointer conversion.
void remove(const irep_namet &name)
const parameterst & parameters() const
bool standard_conversion_pointer_to_member(const exprt &expr, const typet &type, exprt &new_expr)
Pointer-to-member conversion.
bool static_typecast(const exprt &expr, const typet &type, exprt &new_expr, bool check_constantness=true)
C++ Language Type Checking.
bool standard_conversion_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Integral conversion.
floatbv_typet double_type()
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
std::size_t get_width() const
bool user_defined_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
User-defined conversion sequence.
bool reference_related(const exprt &expr, const typet &type) const
Reference-related.
reference_typet reference_type(const typet &subtype)
Deprecated expression utility functions.
bool standard_conversion_qualification(const exprt &expr, const typet &, exprt &new_expr) const
Qualification conversion.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Structure type, corresponds to C style structs.
bool const_typecast(const exprt &expr, const typet &type, exprt &new_expr)
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)
bool cast_away_constness(const typet &t1, const typet &t2) const
void implicit_typecast(exprt &expr, const typet &type) override
bool standard_conversion_pointer(const exprt &expr, const typet &type, exprt &new_expr)
Pointer conversion.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
const typet & return_type() const
bool standard_conversion_floating_integral_conversion(const exprt &expr, const typet &type, exprt &new_expr) const
Floating-integral conversion.
bool implicit_conversion_sequence(const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank)
implicit conversion sequence
bool dynamic_typecast(const exprt &expr, const typet &type, exprt &new_expr)
std::string to_string(const typet &) override
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
API to expression classes.
const source_locationt & source_location() const
bool is_incomplete() const
A struct/union may be incomplete.
An expression containing a side effect.