cprover
|
#include <pointer_logic.h>
Classes | |
struct | pointert |
Public Types | |
typedef hash_numbering< exprt, irep_hash > | objectst |
Public Member Functions | |
exprt | pointer_expr (const pointert &pointer, const typet &type) const |
exprt | pointer_expr (std::size_t object, const typet &type) const |
~pointer_logict () | |
pointer_logict (const namespacet &_ns) | |
std::size_t | add_object (const exprt &expr) |
std::size_t | get_null_object () const |
std::size_t | get_invalid_object () const |
bool | is_dynamic_object (const exprt &expr) const |
void | get_dynamic_objects (std::vector< std::size_t > &objects) const |
Public Attributes | |
objectst | objects |
Protected Member Functions | |
exprt | pointer_expr (const mp_integer &offset, const exprt &object) const |
exprt | object_rec (const mp_integer &offset, const typet &pointer_type, const exprt &src) const |
Protected Attributes | |
const namespacet & | ns |
std::size_t | null_object |
std::size_t | invalid_object |
Definition at line 23 of file pointer_logic.h.
typedef hash_numbering<exprt, irep_hash> pointer_logict::objectst |
Definition at line 27 of file pointer_logic.h.
pointer_logict::~pointer_logict | ( | ) |
Definition at line 206 of file pointer_logic.cpp.
|
explicit |
Definition at line 196 of file pointer_logic.cpp.
References invalid_object, null_object, hash_numbering< T, hash_fkt >::number(), and objects.
std::size_t pointer_logict::add_object | ( | const exprt & | expr | ) |
Definition at line 48 of file pointer_logic.cpp.
References irept::id(), hash_numbering< T, hash_fkt >::number(), objects, exprt::op0(), and exprt::operands().
Referenced by bv_pointerst::add_addr(), dplib_convt::convert_address_of_rec(), cvc_convt::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), and smt2_convt::convert_address_of_rec().
void pointer_logict::get_dynamic_objects | ( | std::vector< std::size_t > & | objects | ) | const |
Definition at line 35 of file pointer_logic.cpp.
References is_dynamic_object(), and objects.
Referenced by smt1_convt::convert_is_dynamic_object(), and smt2_convt::convert_is_dynamic_object().
|
inline |
Definition at line 66 of file pointer_logic.h.
References invalid_object.
Referenced by smt1_convt::convert_expr(), smt2_convt::convert_expr(), and bv_pointerst::convert_rest().
|
inline |
Definition at line 60 of file pointer_logic.h.
References null_object.
Referenced by bv_pointerst::convert_address_of_rec(), smt1_convt::convert_constant(), cvc_convt::convert_constant_expr(), dplib_convt::convert_dplib_expr(), bv_pointerst::convert_pointer_type(), and bv_pointerst::convert_rest().
bool pointer_logict::is_dynamic_object | ( | const exprt & | expr | ) | const |
Definition at line 22 of file pointer_logic.cpp.
References irept::get_bool(), has_prefix(), irept::id(), id2string(), to_symbol_expr(), and exprt::type().
Referenced by bv_pointerst::do_postponed(), and get_dynamic_objects().
|
protected |
Definition at line 125 of file pointer_logic.cpp.
References from_integer(), irept::id(), index_exprt::index(), ns, exprt::op0(), pointer_offset_size(), pointer_type(), member_exprt::set_component_name(), typet::subtype(), to_struct_type(), and exprt::type().
Referenced by pointer_expr().
Definition at line 74 of file pointer_logic.cpp.
References exprt::copy_to_operands(), from_integer(), irept::id(), invalid_object, null_object, pointer_logict::pointert::object, object_rec(), objects, pointer_logict::pointert::offset, pointer_diff_type(), and constant_exprt::set_value().
Referenced by bv_pointerst::bv_get_rec(), smt1_convt::ce_value(), smt2_convt::parse_rec(), and pointer_expr().
Definition at line 66 of file pointer_logic.cpp.
References pointer_expr().
|
protected |
|
protected |
Definition at line 77 of file pointer_logic.h.
Referenced by get_invalid_object(), pointer_expr(), and pointer_logict().
|
protected |
Definition at line 76 of file pointer_logic.h.
Referenced by object_rec().
|
protected |
Definition at line 77 of file pointer_logic.h.
Referenced by get_null_object(), pointer_expr(), and pointer_logict().
objectst pointer_logict::objects |
Definition at line 28 of file pointer_logic.h.
Referenced by add_object(), smt2_convt::define_object_size(), bv_pointerst::do_postponed(), get_dynamic_objects(), pointer_expr(), and pointer_logict().