CBMC
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
rw_range_sett Class Reference

#include <goto_rw.h>

+ Inheritance diagram for rw_range_sett:
+ Collaboration diagram for rw_range_sett:

Public Types

enum class  get_modet { LHS_W , READ }
 
typedef std::map< irep_idt, std::unique_ptr< range_domain_baset > > objectst
 

Public Member Functions

virtual ~rw_range_sett ()
 
 rw_range_sett (const namespacet &_ns, message_handlert &message_handler)
 
const objectst & get_r_set () const
 
const objectst & get_w_set () const
 
const range_domaint & get_ranges (const std::unique_ptr< range_domain_baset > &ranges) const
 
virtual void get_objects_rec (const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
 
virtual void get_objects_rec (const irep_idt &, goto_programt::const_targett, const typet &type)
 
virtual void get_array_objects (const irep_idt &, goto_programt::const_targett, get_modet, const exprt &)
 
void output (std::ostream &out) const
 

Protected Member Functions

virtual void get_objects_rec (get_modet mode, const exprt &expr)
 
virtual void get_objects_rec (const typet &type)
 
virtual void get_objects_complex_real (get_modet mode, const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size)
 
virtual void get_objects_complex_imag (get_modet mode, const complex_imag_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
 
message_handlert & message_handler
 
objectst r_range_set
 
objectst w_range_set
 

Detailed Description

Definition at line 203 of file goto_rw.h.

Member Typedef Documentation

◆ objectst

typedef std::map<irep_idt, std::unique_ptr<range_domain_baset> > rw_range_sett::objectst

Definition at line 206 of file goto_rw.h.

Member Enumeration Documentation

◆ get_modet

enum rw_range_sett::get_modet
strong
Enumerator
LHS_W 
READ 

Definition at line 232 of file goto_rw.h.

Constructor & Destructor Documentation

◆ ~rw_range_sett()

rw_range_sett::~rw_range_sett ( )
virtual

Definition at line 48 of file goto_rw.cpp.

◆ rw_range_sett()

rw_range_sett::rw_range_sett ( const namespacet &  _ns,
message_handlert &  message_handler 
)
inline

Definition at line 210 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 520 of file goto_rw.cpp.

◆ get_array_objects()

void rw_range_sett::get_array_objects ( const irep_idt &  ,
goto_programt::const_targett  ,
get_modet  mode,
const exprt &  pointer 
)
virtual

Reimplemented in rw_range_set_value_sett.

Definition at line 664 of file goto_rw.cpp.

◆ get_objects_address_of()

void rw_range_sett::get_objects_address_of ( const exprt &  object)
protectedvirtual

Definition at line 468 of file goto_rw.cpp.

◆ 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

Definition at line 322 of file goto_rw.cpp.

◆ 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

Definition at line 144 of file goto_rw.cpp.

◆ get_objects_complex_imag()

void rw_range_sett::get_objects_complex_imag ( get_modet  mode,
const complex_imag_exprt &  expr,
const range_spect &  range_start,
const range_spect &  size 
)
protectedvirtual

Definition at line 91 of file goto_rw.cpp.

◆ get_objects_complex_real()

void rw_range_sett::get_objects_complex_real ( get_modet  mode,
const complex_real_exprt &  expr,
const range_spect &  range_start,
const range_spect &  size 
)
protectedvirtual

Definition at line 82 of file goto_rw.cpp.

◆ 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

Reimplemented in rw_range_set_value_sett.

Definition at line 132 of file goto_rw.cpp.

◆ 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

Reimplemented in rw_guarded_range_set_value_sett.

Definition at line 113 of file goto_rw.cpp.

◆ 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

Definition at line 271 of file goto_rw.cpp.

◆ 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

Definition at line 237 of file goto_rw.cpp.

◆ get_objects_rec() [1/5]

virtual void rw_range_sett::get_objects_rec ( const irep_idt &  ,
goto_programt::const_targett  ,
const typet &  type 
)
inlinevirtual

Reimplemented in rw_guarded_range_set_value_sett, and rw_range_set_value_sett.

Definition at line 243 of file goto_rw.h.

◆ get_objects_rec() [2/5]

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

Reimplemented in rw_guarded_range_set_value_sett, and rw_range_set_value_sett.

Definition at line 234 of file goto_rw.h.

◆ get_objects_rec() [3/5]

void rw_range_sett::get_objects_rec ( const typet &  type)
protectedvirtual

Definition at line 653 of file goto_rw.cpp.

◆ get_objects_rec() [4/5]

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

Definition at line 642 of file goto_rw.cpp.

◆ get_objects_rec() [5/5]

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

Definition at line 540 of file goto_rw.cpp.

◆ 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

Definition at line 186 of file goto_rw.cpp.

◆ 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

Definition at line 366 of file goto_rw.cpp.

◆ 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

Definition at line 440 of file goto_rw.cpp.

◆ get_r_set()

const objectst& rw_range_sett::get_r_set ( ) const
inline

Definition at line 215 of file goto_rw.h.

◆ get_ranges()

const range_domaint& rw_range_sett::get_ranges ( const std::unique_ptr< range_domain_baset > &  ranges) const
inline

Definition at line 226 of file goto_rw.h.

◆ get_w_set()

const objectst& rw_range_sett::get_w_set ( ) const
inline

Definition at line 220 of file goto_rw.h.

◆ output()

void rw_range_sett::output ( std::ostream &  out) const

Definition at line 61 of file goto_rw.cpp.

Member Data Documentation

◆ message_handler

message_handlert& rw_range_sett::message_handler
protected

Definition at line 261 of file goto_rw.h.

◆ ns

const namespacet& rw_range_sett::ns
protected

Definition at line 260 of file goto_rw.h.

◆ r_range_set

objectst rw_range_sett::r_range_set
protected

Definition at line 263 of file goto_rw.h.

◆ w_range_set

objectst rw_range_sett::w_range_set
protected

Definition at line 263 of file goto_rw.h.

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