cprover
|
Pointer Logic. More...
#include "pointer_offset_size.h"
#include "arith_tools.h"
#include "c_types.h"
#include "invariant.h"
#include "namespace.h"
#include "simplify_expr.h"
#include "ssa_expr.h"
#include "std_expr.h"
Go to the source code of this file.
Pointer Logic.
Definition in file pointer_offset_size.cpp.
exprt build_sizeof_expr | ( | const constant_exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 579 of file pointer_offset_size.cpp.
References address_bits(), DATA_INVARIANT, irept::find(), from_integer(), irept::is_not_nil(), exprt::make_typecast(), pointer_offset_bits(), pointer_offset_size(), irept::set(), size_type(), to_integer(), and exprt::type().
Referenced by expr2ct::convert_constant().
mp_integer compute_pointer_offset | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 521 of file pointer_offset_size.cpp.
References index_exprt::array(), compute_pointer_offset(), DATA_INVARIANT, namespace_baset::follow(), member_exprt::get_component_name(), ssa_exprt::get_original_expr(), irept::id(), irept::id_string(), index_exprt::index(), is_ssa_expr(), member_offset(), pointer_offset_size(), member_exprt::struct_op(), typet::subtype(), to_index_expr(), to_integer(), to_member_expr(), to_ssa_expr(), to_struct_type(), to_struct_union_type(), and exprt::type().
Referenced by goto_symext::address_arithmetic(), compute_pointer_offset(), value_sett::eval_pointer_offset(), and simplify_exprt::simplify_pointer_offset().
bool get_subexpression_at_offset | ( | exprt & | result, |
mp_integer | offset, | ||
const typet & | target_type_raw, | ||
const namespacet & | ns | ||
) |
Definition at line 624 of file pointer_offset_size.cpp.
References namespace_baset::follow(), from_integer(), get_subexpression_at_offset(), irept::id(), pointer_offset_size(), to_array_type(), to_struct_type(), and exprt::type().
Referenced by value_set_dereferencet::build_reference_to(), and get_subexpression_at_offset().
bool get_subexpression_at_offset | ( | exprt & | result, |
const exprt & | offset, | ||
const typet & | target_type, | ||
const namespacet & | ns | ||
) |
Definition at line 682 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 60 of file pointer_offset_size.cpp.
References struct_union_typet::components().
Referenced by interpretert::byte_offset_to_memory_offset(), goto_checkt::check_rec(), compute_pointer_offset(), bv_pointerst::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), smt2_convt::convert_member(), value_sett::get_value_set_rec(), interpretert::memory_offset_to_byte_offset(), dereferencet::read_object(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_byte_update(), and simplify_exprt::simplify_member().
mp_integer member_offset_bits | ( | const struct_typet & | type, |
const irep_idt & | member, | ||
const namespacet & | ns | ||
) |
Definition at line 80 of file pointer_offset_size.cpp.
References struct_union_typet::components(), and pointer_offset_bits().
Referenced by rw_range_sett::get_objects_member().
exprt member_offset_expr | ( | const member_exprt & | member_expr, |
const namespacet & | ns | ||
) |
Definition at line 253 of file pointer_offset_size.cpp.
References namespace_baset::follow(), from_integer(), member_exprt::get_component_name(), irept::id(), member_offset_expr(), size_type(), member_exprt::struct_op(), to_struct_type(), and exprt::type().
Referenced by build_object_descriptor_rec(), goto_checkt::check_rec(), flatten_byte_extract(), member_offset_expr(), dereferencet::read_object(), and c_typecheck_baset::typecheck_expr_builtin_offsetof().
exprt member_offset_expr | ( | const struct_typet & | type, |
const irep_idt & | member, | ||
const namespacet & | ns | ||
) |
Definition at line 268 of file pointer_offset_size.cpp.
References struct_union_typet::components(), DATA_INVARIANT, 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 114 of file pointer_offset_size.cpp.
References struct_union_typet::components(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::get_bool(), bitvector_typet::get_width(), irept::id(), pointer_offset_bits(), array_typet::size(), vector_typet::size(), typet::subtype(), to_array_type(), to_bitvector_type(), to_c_enum_tag_type(), to_integer(), to_struct_type(), to_union_type(), and to_vector_type().
Referenced by add_padding(), as_vcd_binary(), simplify_exprt::bits2expr(), endianness_mapt::build_big_endian(), endianness_mapt::build_little_endian(), build_sizeof_expr(), expr2ct::convert_with_precedence(), linkingt::duplicate_code_symbol(), expr_initializert< nondet >::expr_initializer_rec(), 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(), lower_popcount(), member_offset_bits(), value_set_dereferencet::memory_model(), output_vcd(), goto_symext::phi_function(), pointer_offset_bits(), pointer_offset_bits_as_string(), pointer_offset_size(), print_global_state_size(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_pointer_offset(), size_of_expr(), goto_symext::symex_assign_symbol(), goto_symext::symex_goto(), rd_range_domaint::transform_function_call(), c_typecheck_baset::typecheck_expr_typecast(), and unpack_rec().
mp_integer pointer_offset_size | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Compute the size of a type in bytes, rounding up to full bytes.
Definition at line 104 of file pointer_offset_size.cpp.
References pointer_offset_bits().
Referenced by add_padding_gcc(), add_padding_msvc(), alignment(), value_set_dereferencet::build_reference_to(), build_sizeof_expr(), interpretert::byte_offset_to_memory_offset(), compute_pointer_offset(), bv_pointerst::convert_address_of_rec(), bv_pointerst::convert_bitvector(), boolbvt::convert_byte_extract(), boolbvt::convert_index(), smt2_convt::convert_minus(), 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(), interpretert::memory_offset_to_byte_offset(), pointer_logict::object_rec(), 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(), and goto_symext::symex_allocate().
exprt size_of_expr | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Definition at line 311 of file pointer_offset_size.cpp.
References struct_union_typet::components(), DATA_INVARIANT, namespace_baset::follow(), namespace_baset::follow_tag(), from_integer(), irept::get_bool(), bitvector_typet::get_width(), irept::id(), irept::is_nil(), exprt::make_typecast(), pointer_offset_bits(), 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 allocate_dynamic_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(), bv_pointerst::do_postponed(), flatten_byte_extract(), good_pointer_def(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), member_offset_expr(), value_set_dereferencet::memory_model_bytes(), mm_io(), goto_symext::process_array_expr(), dereferencet::read_object(), simplify_exprt::simplify_object_size(), size_of_expr(), goto_symext::symex_other(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_sizeof(), c_typecheck_baset::typecheck_vector_type(), and cpp_typecheckt::zero_initializer().