cprover
|
Pointer Logic. More...
Go to the source code of this file.
Classes | |
class | member_offset_iterator |
Functions | |
mp_integer | member_offset (const struct_typet &type, const irep_idt &member, const namespacet &ns) |
mp_integer | pointer_offset_size (const typet &type, const namespacet &ns) |
mp_integer | pointer_offset_bits (const typet &type, const namespacet &ns) |
mp_integer | compute_pointer_offset (const exprt &expr, const namespacet &ns) |
exprt | member_offset_expr (const member_exprt &, const namespacet &ns) |
exprt | member_offset_expr (const struct_typet &type, const irep_idt &member, const namespacet &ns) |
exprt | size_of_expr (const typet &type, const namespacet &ns) |
exprt | build_sizeof_expr (const constant_exprt &expr, const namespacet &ns) |
bool | get_subexpression_at_offset (exprt &result, mp_integer offset, const typet &target_type, const namespacet &ns) |
bool | get_subexpression_at_offset (exprt &result, const exprt &offset, const typet &target_type, const namespacet &ns) |
Pointer Logic.
Definition in file pointer_offset_size.h.
exprt build_sizeof_expr | ( | const constant_exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 533 of file pointer_offset_size.cpp.
References address_bits(), configt::ansi_c, config, irept::find(), from_integer(), irept::is_not_nil(), exprt::make_typecast(), pointer_offset_size(), configt::ansi_ct::pointer_width, irept::set(), size_type(), to_integer(), member_offset_iterator::type, and exprt::type().
Referenced by expr2ct::convert_constant(), and member_offset_iterator::operator->().
mp_integer compute_pointer_offset | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 474 of file pointer_offset_size.cpp.
References compute_pointer_offset(), namespace_baset::follow(), irept::get(), ssa_exprt::get_original_expr(), irept::id(), is_ssa_expr(), member_offset(), member_offset_iterator::ns, exprt::op0(), exprt::op1(), exprt::operands(), pointer_offset_size(), to_integer(), to_ssa_expr(), to_struct_type(), member_offset_iterator::type, and exprt::type().
Referenced by goto_symext::address_arithmetic(), compute_pointer_offset(), value_sett::eval_pointer_offset(), member_offset_iterator::operator->(), and simplify_exprt::simplify_pointer_offset().
bool get_subexpression_at_offset | ( | exprt & | result, |
mp_integer | offset, | ||
const typet & | target_type, | ||
const namespacet & | ns | ||
) |
Definition at line 576 of file pointer_offset_size.cpp.
References namespace_baset::follow(), from_integer(), get_subexpression_at_offset(), irept::id(), member_offset_iterator::ns, pointer_offset_size(), to_array_type(), to_struct_type(), and exprt::type().
Referenced by value_set_dereferencet::build_reference_to(), get_subexpression_at_offset(), and member_offset_iterator::operator->().
bool get_subexpression_at_offset | ( | exprt & | result, |
const exprt & | offset, | ||
const typet & | target_type, | ||
const namespacet & | ns | ||
) |
Definition at line 634 of file pointer_offset_size.cpp.
References get_subexpression_at_offset(), and to_integer().
mp_integer member_offset | ( | const struct_typet & | type, |
const irep_idt & | member, | ||
const namespacet & | ns | ||
) |
Definition at line 63 of file pointer_offset_size.cpp.
References struct_union_typet::components().
Referenced by goto_checkt::check_rec(), compute_pointer_offset(), dplib_convt::convert_address_of_rec(), cvc_convt::convert_address_of_rec(), bv_pointerst::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), smt2_convt::convert_member(), rw_range_sett::get_objects_member(), value_sett::get_value_set_rec(), member_offset_iterator::operator->(), dereferencet::read_object(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_byte_update(), and simplify_exprt::simplify_member().
exprt member_offset_expr | ( | const member_exprt & | , |
const namespacet & | ns | ||
) |
Definition at line 231 of file pointer_offset_size.cpp.
References namespace_baset::follow(), from_integer(), member_exprt::get_component_name(), irept::id(), member_offset_expr(), member_offset_iterator::ns, size_type(), member_exprt::struct_op(), to_struct_type(), member_offset_iterator::type, and exprt::type().
Referenced by build_object_descriptor_rec(), goto_checkt::check_rec(), flatten_byte_extract(), member_offset_expr(), member_offset_iterator::operator->(), and dereferencet::read_object().
exprt member_offset_expr | ( | const struct_typet & | type, |
const irep_idt & | member, | ||
const namespacet & | ns | ||
) |
Definition at line 246 of file pointer_offset_size.cpp.
References member_offset_iterator::bit_field_bits, struct_union_typet::components(), from_integer(), irept::is_nil(), simplify(), size_of_expr(), size_type(), to_c_bit_field_type(), and exprt::type().
mp_integer pointer_offset_bits | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Definition at line 93 of file pointer_offset_size.cpp.
References configt::ansi_c, struct_union_typet::components(), config, namespace_baset::follow(), namespace_baset::follow_tag(), bitvector_typet::get_width(), irept::id(), member_offset_iterator::ns, pointer_offset_bits(), configt::ansi_ct::pointer_width, array_typet::size(), vector_typet::size(), typet::subtype(), to_array_type(), to_bitvector_type(), to_c_bit_field_type(), to_c_enum_tag_type(), to_integer(), to_struct_type(), to_union_type(), and to_vector_type().
Referenced by add_padding(), simplify_exprt::bits2expr(), endianness_mapt::build_big_endian(), endianness_mapt::build_little_endian(), expr2ct::convert_with_precedence(), linkingt::duplicate_code_symbol(), flatten_byte_extract(), flatten_byte_update(), rw_range_sett::get_objects_array(), rw_range_sett::get_objects_byte_extract(), rw_range_sett::get_objects_complex(), rw_range_set_value_sett::get_objects_dereference(), rw_range_sett::get_objects_index(), rw_range_sett::get_objects_rec(), rw_range_sett::get_objects_shift(), rw_range_sett::get_objects_struct(), rw_range_sett::get_objects_typecast(), member_offset_iterator::operator->(), output_vcd(), pointer_offset_bits(), pointer_offset_size(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), rd_range_domaint::transform_function_call(), c_typecheck_baset::typecheck_expr_typecast(), unpack_rec(), and zero_initializert::zero_initializer_rec().
mp_integer pointer_offset_size | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Definition at line 83 of file pointer_offset_size.cpp.
References pointer_offset_bits().
Referenced by add_padding(), as_vcd_binary(), value_set_dereferencet::build_reference_to(), build_sizeof_expr(), compute_pointer_offset(), bv_pointerst::convert_address_of_rec(), bv_pointerst::convert_bitvector(), smt2_convt::convert_minus(), smt1_convt::convert_plus(), smt2_convt::convert_plus(), bv_pointerst::convert_pointer_type(), flatten_byte_update(), value_sett::get_reference_set_rec(), get_subexpression_at_offset(), value_sett::get_value_set_rec(), value_set_dereferencet::memory_model_bytes(), pointer_logict::object_rec(), member_offset_iterator::operator++(), member_offset_iterator::operator->(), print_struct_alignment_problems(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_index(), simplify_exprt::simplify_member(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_typecast(), size_of_expr(), path_symext::symex_malloc(), and goto_symext::symex_malloc().
exprt size_of_expr | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Definition at line 287 of file pointer_offset_size.cpp.
References configt::ansi_c, member_offset_iterator::bit_field_bits, struct_union_typet::components(), config, namespace_baset::follow(), namespace_baset::follow_tag(), from_integer(), bitvector_typet::get_width(), irept::id(), irept::is_nil(), exprt::make_typecast(), member_offset_iterator::ns, pointer_offset_size(), configt::ansi_ct::pointer_width, simplify(), array_typet::size(), vector_typet::size(), size_of_expr(), size_type(), typet::subtype(), to_array_type(), to_bitvector_type(), to_c_bit_field_type(), to_c_enum_tag_type(), to_struct_type(), to_union_type(), to_vector_type(), and exprt::type().
Referenced by java_object_factoryt::allocate_object(), goto_checkt::bounds_check(), build_object_descriptor_rec(), value_set_dereferencet::build_reference_to(), goto_checkt::check_rec(), smt2_convt::define_object_size(), dereferencet::dereference_plus(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), bv_pointerst::do_postponed(), flatten_byte_extract(), good_pointer_def(), member_offset_expr(), value_set_dereferencet::memory_model_bytes(), mm_io(), member_offset_iterator::operator->(), dereferencet::read_object(), simplify_exprt::simplify_object_size(), and size_of_expr().