cprover
rw_range_set_value_sett Class Reference

#include <goto_rw.h>

Inheritance diagram for rw_range_set_value_sett:
[legend]
Collaboration diagram for rw_range_set_value_sett:
[legend]

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, 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)
 
- Public Member Functions inherited from rw_range_sett
virtual ~rw_range_sett ()
 
 rw_range_sett (const namespacet &_ns)
 
const objectstget_r_set () const
 
const objectstget_w_set () const
 
const range_domaintget_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)
 
- Protected Member Functions inherited from rw_range_sett
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_setstvalue_sets
 
goto_programt::const_targett target
 
- Protected Attributes inherited from rw_range_sett
const namespacetns
 
objectst r_range_set
 
objectst w_range_set
 

Additional Inherited Members

- Public Types inherited from rw_range_sett
enum  get_modet { get_modet::LHS_W, get_modet::READ }
 
typedef std::unordered_map< irep_idt, std::unique_ptr< range_domain_baset >, string_hashobjectst
 

Detailed Description

Definition at line 251 of file goto_rw.h.

Constructor & Destructor Documentation

◆ rw_range_set_value_sett()

rw_range_set_value_sett::rw_range_set_value_sett ( const namespacet _ns,
value_setst _value_sets 
)
inline

Definition at line 254 of file goto_rw.h.

Member Function Documentation

◆ get_objects_dereference()

void rw_range_set_value_sett::get_objects_dereference ( get_modet  mode,
const dereference_exprt deref,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

◆ get_objects_rec() [1/5]

void rw_range_sett::get_objects_rec

Definition at line 484 of file goto_rw.cpp.

◆ get_objects_rec() [2/5]

void rw_range_sett::get_objects_rec

Definition at line 575 of file goto_rw.cpp.

◆ get_objects_rec() [3/5]

void rw_range_sett::get_objects_rec

Definition at line 582 of file goto_rw.cpp.

◆ get_objects_rec() [4/5]

virtual void rw_range_sett::get_objects_rec
inline

Definition at line 143 of file goto_rw.h.

◆ get_objects_rec() [5/5]

virtual void rw_range_set_value_sett::get_objects_rec ( goto_programt::const_targett  _target,
get_modet  mode,
const exprt expr 
)
inlinevirtual

Member Data Documentation

◆ target

goto_programt::const_targett rw_range_set_value_sett::target
protected

Definition at line 277 of file goto_rw.h.

Referenced by get_objects_dereference(), and get_objects_rec().

◆ value_sets

value_setst& rw_range_set_value_sett::value_sets
protected

Definition at line 275 of file goto_rw.h.

Referenced by get_objects_dereference().


The documentation for this class was generated from the following files: