cprover
|
#include <goto_rw.h>
Public Types | |
enum | get_modet { get_modet::LHS_W, get_modet::READ } |
typedef std::unordered_map< irep_idt, std::unique_ptr< 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, 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, std::unique_ptr<range_domain_baset>, string_hash> rw_range_sett::objectst |
|
strong |
|
virtual |
Definition at line 51 of file goto_rw.cpp.
References r_range_set, and w_range_set.
|
inlineexplicit |
|
protectedvirtual |
Reimplemented in rw_guarded_range_set_value_sett.
Definition at line 464 of file goto_rw.cpp.
References LHS_W, r_range_set, and w_range_set.
Referenced by get_objects_rec().
|
protectedvirtual |
Definition at line 414 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(), unary_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().
Referenced by get_objects_rec().
|
protectedvirtual |
Definition at line 289 of file goto_rw.cpp.
References namespace_baset::follow(), forall_operands, get_objects_rec(), ns, exprt::operands(), pointer_offset_bits(), typet::subtype(), to_array_type(), to_range_spect(), and exprt::type().
Referenced by get_objects_rec().
|
protectedvirtual |
Definition at line 134 of file goto_rw.cpp.
References get_objects_rec(), irept::id(), integer2size_t(), ns, byte_extract_exprt::offset(), byte_extract_exprt::op(), pointer_offset_bits(), simplify_expr(), to_integer(), and exprt::type().
Referenced by get_objects_rec().
|
protectedvirtual |
Definition at line 85 of file goto_rw.cpp.
References get_objects_rec(), irept::id(), ns, exprt::op0(), pointer_offset_bits(), typet::subtype(), to_range_spect(), and exprt::type().
Referenced by get_objects_rec().
|
protectedvirtual |
Reimplemented in rw_range_set_value_sett.
Definition at line 122 of file goto_rw.cpp.
References get_objects_rec(), dereference_exprt::pointer(), and READ.
Referenced by rw_range_set_value_sett::get_objects_dereference(), and get_objects_rec().
|
protectedvirtual |
Reimplemented in rw_guarded_range_set_value_sett.
Definition at line 103 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().
Referenced by get_objects_rec().
|
protectedvirtual |
Definition at line 239 of file goto_rw.cpp.
References index_exprt::array(), namespace_baset::follow(), get_objects_rec(), irept::id(), index_exprt::index(), ns, pointer_offset_bits(), READ, simplify_expr(), typet::subtype(), to_array_type(), to_integer(), to_range_spect(), to_vector_type(), and exprt::type().
Referenced by get_objects_rec().
|
protectedvirtual |
Definition at line 209 of file goto_rw.cpp.
References namespace_baset::follow(), member_exprt::get_component_name(), get_objects_rec(), irept::id(), member_offset_bits(), ns, member_exprt::struct_op(), to_range_spect(), to_struct_type(), and exprt::type().
Referenced by get_objects_rec().
|
inlinevirtual |
Reimplemented in rw_guarded_range_set_value_sett, and rw_range_set_value_sett.
Definition at line 143 of file goto_rw.h.
Referenced by get_objects_address_of(), get_objects_array(), get_objects_byte_extract(), get_objects_complex(), get_objects_dereference(), get_objects_if(), get_objects_index(), get_objects_member(), get_objects_rec(), rw_range_set_value_sett::get_objects_rec(), get_objects_shift(), get_objects_struct(), get_objects_typecast(), and goto_rw().
|
virtual |
Definition at line 582 of file goto_rw.cpp.
References get_objects_rec(), irept::id(), READ, typet::subtype(), and to_array_type().
Definition at line 575 of file goto_rw.cpp.
References get_objects_rec(), ns, pointer_offset_bits(), to_range_spect(), and exprt::type().
|
protectedvirtual |
Definition at line 484 of file goto_rw.cpp.
References add(), forall_operands, symbol_exprt::get_identifier(), get_objects_address_of(), get_objects_array(), get_objects_byte_extract(), get_objects_complex(), get_objects_dereference(), get_objects_if(), get_objects_index(), get_objects_member(), get_objects_rec(), get_objects_shift(), get_objects_struct(), get_objects_typecast(), irept::id(), irept::id_string(), LHS_W, ns, 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 161 of file goto_rw.cpp.
References shift_exprt::distance(), get_objects_rec(), irept::id(), ns, shift_exprt::op(), pointer_offset_bits(), simplify_expr(), to_integer(), to_range_spect(), and exprt::type().
Referenced by get_objects_rec().
|
protectedvirtual |
Definition at line 329 of file goto_rw.cpp.
References namespace_baset::follow(), forall_operands, get_objects_rec(), ns, pointer_offset_bits(), to_range_spect(), to_struct_type(), and exprt::type().
Referenced by get_objects_rec().
|
protectedvirtual |
Definition at line 389 of file goto_rw.cpp.
References get_objects_rec(), ns, unary_exprt::op(), pointer_offset_bits(), to_range_spect(), and exprt::type().
Referenced by get_objects_rec().
|
inline |
Definition at line 125 of file goto_rw.h.
References r_range_set.
|
inline |
Definition at line 135 of file goto_rw.h.
References PRECONDITION.
Referenced by dep_graph_domaint::data_dependencies().
|
inline |
Definition at line 130 of file goto_rw.h.
References w_range_set.
void rw_range_sett::output | ( | std::ostream & | out | ) | const |
Definition at line 64 of file goto_rw.cpp.
References forall_rw_range_set_r_objects, forall_rw_range_set_w_objects, and ns.
Referenced by operator<<().
|
protected |
Definition at line 156 of file goto_rw.h.
Referenced by get_objects_array(), get_objects_byte_extract(), get_objects_complex(), rw_range_set_value_sett::get_objects_dereference(), get_objects_index(), get_objects_member(), get_objects_rec(), get_objects_shift(), get_objects_struct(), get_objects_typecast(), and output().
|
protected |
Definition at line 158 of file goto_rw.h.
Referenced by add(), rw_guarded_range_set_value_sett::add(), get_r_set(), and ~rw_range_sett().
|
protected |
Definition at line 158 of file goto_rw.h.
Referenced by add(), rw_guarded_range_set_value_sett::add(), get_w_set(), and ~rw_range_sett().