cprover
rw_range_sett Class Reference

#include <goto_rw.h>

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

Public Types

enum  get_modet { get_modet::LHS_W, get_modet::READ }
 
typedef std::unordered_map< irep_idt, range_domain_baset *, string_hashobjectst
 

Public Member Functions

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 (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 namespacetns
 
objectst r_range_set
 
objectst w_range_set
 

Detailed Description

Definition at line 82 of file goto_rw.h.

Member Typedef Documentation

§ objectst

Definition at line 89 of file goto_rw.h.

Member Enumeration Documentation

§ get_modet

Enumerator
LHS_W 
READ 

Definition at line 115 of file goto_rw.h.

Constructor & Destructor Documentation

§ ~rw_range_sett()

rw_range_sett::~rw_range_sett ( )
virtual

Definition at line 47 of file goto_rw.cpp.

§ rw_range_sett()

rw_range_sett::rw_range_sett ( const namespacet _ns)
inlineexplicit

Definition at line 94 of file goto_rw.h.

Member Function Documentation

§ add()

void rw_range_sett::add ( get_modet  mode,
const irep_idt identifier,
const range_spect range_start,
const range_spect range_end 
)
protectedvirtual

Reimplemented in rw_guarded_range_set_value_sett.

Definition at line 458 of file goto_rw.cpp.

References LHS_W.

§ get_objects_address_of()

§ get_objects_array()

void rw_range_sett::get_objects_array ( get_modet  mode,
const array_exprt expr,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

§ get_objects_byte_extract()

void rw_range_sett::get_objects_byte_extract ( get_modet  mode,
const byte_extract_exprt be,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

§ get_objects_complex()

void rw_range_sett::get_objects_complex ( get_modet  mode,
const exprt expr,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

§ get_objects_dereference()

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

§ get_objects_if()

void rw_range_sett::get_objects_if ( get_modet  mode,
const if_exprt if_expr,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

§ get_objects_index()

void rw_range_sett::get_objects_index ( get_modet  mode,
const index_exprt expr,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

§ get_objects_member()

void rw_range_sett::get_objects_member ( get_modet  mode,
const member_exprt expr,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

§ get_objects_rec() [1/4]

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

§ get_objects_rec() [2/4]

void rw_range_sett::get_objects_rec ( const typet type)
virtual

Definition at line 574 of file goto_rw.cpp.

References get_objects_rec(), irept::id(), READ, typet::subtype(), and to_array_type().

§ get_objects_rec() [3/4]

void rw_range_sett::get_objects_rec ( get_modet  mode,
const exprt expr 
)
protectedvirtual

Definition at line 567 of file goto_rw.cpp.

References get_objects_rec(), pointer_offset_bits(), to_range_spect(), and exprt::type().

§ get_objects_rec() [4/4]

§ get_objects_shift()

void rw_range_sett::get_objects_shift ( get_modet  mode,
const shift_exprt shift,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

§ get_objects_struct()

void rw_range_sett::get_objects_struct ( get_modet  mode,
const struct_exprt expr,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

§ get_objects_typecast()

void rw_range_sett::get_objects_typecast ( get_modet  mode,
const typecast_exprt tc,
const range_spect range_start,
const range_spect size 
)
protectedvirtual

§ get_r_set()

const objectst& rw_range_sett::get_r_set ( ) const
inline

Definition at line 99 of file goto_rw.h.

§ get_ranges()

const range_domaint& rw_range_sett::get_ranges ( objectst::const_iterator  it) const
inline

Definition at line 109 of file goto_rw.h.

References PRECONDITION.

Referenced by dep_graph_domaint::data_dependencies().

§ get_w_set()

const objectst& rw_range_sett::get_w_set ( ) const
inline

Definition at line 104 of file goto_rw.h.

§ output()

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<<().

Member Data Documentation

§ ns

const namespacet& rw_range_sett::ns
protected

Definition at line 130 of file goto_rw.h.

§ r_range_set

objectst rw_range_sett::r_range_set
protected

Definition at line 132 of file goto_rw.h.

§ w_range_set

objectst rw_range_sett::w_range_set
protected

Definition at line 132 of file goto_rw.h.


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