cprover
|
#include <goto_rw.h>
Public Types | |
enum | get_modet { get_modet::LHS_W, get_modet::READ } |
typedef std::unordered_map< irep_idt, range_domain_baset *, string_hash > | objectst |
Public Member Functions | |
virtual | ~rw_range_sett () |
rw_range_sett (const namespacet &_ns) | |
const objectst & | get_r_set () const |
const objectst & | get_w_set () const |
const range_domaint & | get_ranges (objectst::const_iterator it) const |
virtual void | get_objects_rec (goto_programt::const_targett _target, get_modet mode, const exprt &expr) |
virtual void | get_objects_rec (const typet &type) |
void | output (std::ostream &out) const |
Protected Member Functions | |
virtual void | get_objects_rec (get_modet mode, const exprt &expr) |
virtual void | get_objects_complex (get_modet mode, const exprt &expr, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_if (get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_dereference (get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_byte_extract (get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_shift (get_modet mode, const shift_exprt &shift, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_member (get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_index (get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_array (get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_struct (get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_typecast (get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size) |
virtual void | get_objects_address_of (const exprt &object) |
virtual void | get_objects_rec (get_modet mode, const exprt &expr, const range_spect &range_start, const range_spect &size) |
virtual void | add (get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) |
Protected Attributes | |
const namespacet & | ns |
objectst | r_range_set |
objectst | w_range_set |
typedef std::unordered_map<irep_idt, range_domain_baset*, string_hash> rw_range_sett::objectst |
|
strong |
|
virtual |
Definition at line 47 of file goto_rw.cpp.
|
inlineexplicit |
|
protectedvirtual |
Reimplemented in rw_guarded_range_set_value_sett.
Definition at line 458 of file goto_rw.cpp.
References LHS_W.
|
protectedvirtual |
Definition at line 408 of file goto_rw.cpp.
References index_exprt::array(), if_exprt::cond(), if_exprt::false_case(), get_objects_rec(), index_exprt::index(), byte_extract_exprt::op(), typecast_exprt::op(), READ, member_exprt::struct_op(), to_byte_extract_expr(), to_if_expr(), to_index_expr(), to_member_expr(), to_typecast_expr(), and if_exprt::true_case().
|
protectedvirtual |
Definition at line 283 of file goto_rw.cpp.
References forall_operands, get_objects_rec(), exprt::operands(), pointer_offset_bits(), typet::subtype(), to_array_type(), to_range_spect(), and exprt::type().
|
protectedvirtual |
Definition at line 130 of file goto_rw.cpp.
References get_objects_rec(), irept::id(), integer2size_t(), byte_extract_exprt::offset(), byte_extract_exprt::op(), pointer_offset_bits(), simplify_expr(), to_integer(), and exprt::type().
|
protectedvirtual |
Definition at line 81 of file goto_rw.cpp.
References get_objects_rec(), irept::id(), exprt::op0(), pointer_offset_bits(), typet::subtype(), to_range_spect(), and exprt::type().
|
protectedvirtual |
Reimplemented in rw_range_set_value_sett.
Definition at line 118 of file goto_rw.cpp.
References get_objects_rec(), dereference_exprt::pointer(), and READ.
Referenced by rw_range_set_value_sett::get_objects_dereference().
|
protectedvirtual |
Reimplemented in rw_guarded_range_set_value_sett.
Definition at line 99 of file goto_rw.cpp.
References if_exprt::cond(), if_exprt::false_case(), get_objects_rec(), exprt::is_false(), exprt::is_true(), READ, and if_exprt::true_case().
|
protectedvirtual |
Definition at line 235 of file goto_rw.cpp.
References index_exprt::array(), get_objects_rec(), irept::id(), index_exprt::index(), pointer_offset_bits(), READ, simplify_expr(), typet::subtype(), to_array_type(), to_integer(), to_range_spect(), to_vector_type(), and exprt::type().
|
protectedvirtual |
Definition at line 205 of file goto_rw.cpp.
References member_exprt::get_component_name(), get_objects_rec(), irept::id(), member_offset(), member_exprt::struct_op(), to_range_spect(), to_struct_type(), and exprt::type().
|
inlinevirtual |
Reimplemented in rw_guarded_range_set_value_sett, and rw_range_set_value_sett.
Definition at line 117 of file goto_rw.h.
References get_objects_rec(), and range_domain_baset::output().
Referenced by rw_range_set_value_sett::get_objects_rec(), goto_rw(), and rw_range_set_value_sett::rw_range_set_value_sett().
|
virtual |
Definition at line 574 of file goto_rw.cpp.
References get_objects_rec(), irept::id(), READ, typet::subtype(), and to_array_type().
Definition at line 567 of file goto_rw.cpp.
References get_objects_rec(), pointer_offset_bits(), to_range_spect(), and exprt::type().
|
protectedvirtual |
Definition at line 476 of file goto_rw.cpp.
References forall_operands, symbol_exprt::get_identifier(), get_objects_rec(), irept::id(), irept::id_string(), LHS_W, address_of_exprt::object(), pointer_offset_bits(), READ, to_address_of_expr(), to_array_expr(), to_byte_extract_expr(), to_dereference_expr(), to_if_expr(), to_index_expr(), to_member_expr(), to_range_spect(), to_shift_expr(), to_struct_expr(), to_symbol_expr(), to_typecast_expr(), and exprt::type().
|
protectedvirtual |
Definition at line 157 of file goto_rw.cpp.
References shift_exprt::distance(), get_objects_rec(), irept::id(), shift_exprt::op(), pointer_offset_bits(), simplify_expr(), to_integer(), to_range_spect(), and exprt::type().
|
protectedvirtual |
Definition at line 323 of file goto_rw.cpp.
References forall_operands, get_objects_rec(), pointer_offset_bits(), to_range_spect(), to_struct_type(), and exprt::type().
|
protectedvirtual |
Definition at line 383 of file goto_rw.cpp.
References get_objects_rec(), typecast_exprt::op(), pointer_offset_bits(), to_range_spect(), and exprt::type().
|
inline |
Definition at line 109 of file goto_rw.h.
References PRECONDITION.
Referenced by dep_graph_domaint::data_dependencies().
void rw_range_sett::output | ( | std::ostream & | out | ) | const |
Definition at line 60 of file goto_rw.cpp.
References forall_rw_range_set_r_objects, and forall_rw_range_set_w_objects.
Referenced by operator<<().
|
protected |