cprover
|
#include <goto_rw.h>
Public Member Functions | |
rw_range_set_value_sett (const namespacet &_ns, value_setst &_value_sets) | |
virtual void | get_objects_rec (goto_programt::const_targett _target, get_modet mode, const exprt &expr) |
virtual void | get_objects_rec (goto_programt::const_targett _target, get_modet mode, const exprt &expr) |
virtual void | get_objects_rec (const typet &type) |
virtual void | get_objects_rec (get_modet mode, const exprt &expr) |
virtual void | get_objects_rec (get_modet mode, const exprt &expr, const range_spect &range_start, const range_spect &size) |
![]() | |
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 (const typet &type) |
void | output (std::ostream &out) const |
Protected Member Functions | |
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_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_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 | |
value_setst & | value_sets |
goto_programt::const_targett | target |
![]() | |
const namespacet & | ns |
objectst | r_range_set |
objectst | w_range_set |
Additional Inherited Members | |
![]() | |
enum | get_modet { get_modet::LHS_W, get_modet::READ } |
typedef std::unordered_map< irep_idt, range_domain_baset *, string_hash > | objectst |
|
inline |
|
protectedvirtual |
Reimplemented from rw_range_sett.
Definition at line 584 of file goto_rw.cpp.
References dereference(), rw_range_sett::get_objects_dereference(), get_objects_rec(), value_set_dereferencet::has_dereference(), rw_range_sett::ns, pointer_offset_bits(), target, to_range_spect(), and value_sets.
void rw_range_sett::get_objects_rec |
Definition at line 476 of file goto_rw.cpp.
void rw_range_sett::get_objects_rec |
Definition at line 567 of file goto_rw.cpp.
void rw_range_sett::get_objects_rec |
Definition at line 574 of file goto_rw.cpp.
|
inlinevirtual |
Reimplemented from rw_range_sett.
Reimplemented in rw_guarded_range_set_value_sett.
Definition at line 238 of file goto_rw.h.
References rw_range_sett::get_objects_rec(), and target.
Referenced by get_objects_dereference(), and rw_guarded_range_set_value_sett::get_objects_rec().
|
protected |
Definition at line 251 of file goto_rw.h.
Referenced by get_objects_dereference(), and get_objects_rec().
|
protected |
Definition at line 249 of file goto_rw.h.
Referenced by get_objects_dereference().