cprover
pointer_offset_size.cpp File Reference

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"
Include dependency graph for pointer_offset_size.cpp:

Go to the source code of this file.

Functions

mp_integer member_offset (const struct_typet &type, const irep_idt &member, const namespacet &ns)
 
mp_integer member_offset_bits (const struct_typet &type, const irep_idt &member, const namespacet &ns)
 
mp_integer pointer_offset_size (const typet &type, const namespacet &ns)
 Compute the size of a type in bytes, rounding up to full bytes. More...
 
mp_integer pointer_offset_bits (const typet &type, const namespacet &ns)
 
exprt member_offset_expr (const member_exprt &member_expr, 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)
 
mp_integer compute_pointer_offset (const exprt &expr, 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_raw, const namespacet &ns)
 
bool get_subexpression_at_offset (exprt &result, const exprt &offset, const typet &target_type, const namespacet &ns)
 

Detailed Description

Pointer Logic.

Definition in file pointer_offset_size.cpp.

Function Documentation

◆ build_sizeof_expr()

◆ compute_pointer_offset()

◆ get_subexpression_at_offset() [1/2]

bool get_subexpression_at_offset ( exprt result,
mp_integer  offset,
const typet target_type_raw,
const namespacet ns 
)

◆ get_subexpression_at_offset() [2/2]

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().

◆ member_offset()

◆ member_offset_bits()

mp_integer member_offset_bits ( const struct_typet type,
const irep_idt member,
const namespacet ns 
)

◆ member_offset_expr() [1/2]

◆ member_offset_expr() [2/2]

exprt member_offset_expr ( const struct_typet type,
const irep_idt member,
const namespacet ns 
)

◆ pointer_offset_bits()

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().

◆ pointer_offset_size()

◆ size_of_expr()