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

#include <goto_rw.h>

+ Inheritance diagram for rw_guarded_range_set_value_sett:
+ Collaboration diagram for rw_guarded_range_set_value_sett:

Public Member Functions

 rw_guarded_range_set_value_sett (const namespacet &_ns, value_setst &_value_sets, guard_managert &guard_manager, message_handlert &message_handler)
 
const guarded_range_domaint & get_ranges (const std::unique_ptr< range_domain_baset > &ranges) const
 
void get_objects_rec (const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &expr) override
 
void get_objects_rec (const irep_idt &function, goto_programt::const_targett target, const typet &type) override
 
- Public Member Functions inherited from rw_range_set_value_sett
 rw_range_set_value_sett (const namespacet &_ns, value_setst &_value_sets, message_handlert &message_handler)
 
void get_array_objects (const irep_idt &_function, goto_programt::const_targett _target, get_modet mode, const exprt &pointer) override
 
- Public Member Functions inherited from rw_range_sett
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
 
void output (std::ostream &out) const
 

Protected Member Functions

void get_objects_if (get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size) override
 
void add (get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
 
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_objects_rec (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, const range_spect &range_start, const range_spect &size)
 
- Protected Member Functions inherited from rw_range_set_value_sett
void get_objects_dereference (get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size) override
 
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_objects_rec (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, 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_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_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)
 

Protected Attributes

guard_managert & guard_manager
 
guardt guard
 
- Protected Attributes inherited from rw_range_set_value_sett
value_setst & value_sets
 
irep_idt function
 
goto_programt::const_targett target
 
- Protected Attributes inherited from rw_range_sett
const namespacet & ns
 
message_handlert & message_handler
 
objectst r_range_set
 
objectst w_range_set
 

Additional Inherited Members

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

Detailed Description

Definition at line 456 of file goto_rw.h.

Constructor & Destructor Documentation

◆ rw_guarded_range_set_value_sett()

rw_guarded_range_set_value_sett::rw_guarded_range_set_value_sett ( const namespacet &  _ns,
value_setst &  _value_sets,
guard_managert &  guard_manager,
message_handlert &  message_handler 
)
inline

Definition at line 459 of file goto_rw.h.

Member Function Documentation

◆ add()

void rw_guarded_range_set_value_sett::add ( get_modet  mode,
const irep_idt &  identifier,
const range_spect &  range_start,
const range_spect &  range_end 
)
overrideprotectedvirtual

Reimplemented from rw_range_sett.

Definition at line 758 of file goto_rw.cpp.

◆ get_objects_if()

void rw_guarded_range_set_value_sett::get_objects_if ( get_modet  mode,
const if_exprt &  if_expr,
const range_spect &  range_start,
const range_spect &  size 
)
overrideprotectedvirtual

Reimplemented from rw_range_sett.

Definition at line 732 of file goto_rw.cpp.

◆ get_objects_rec() [1/7]

virtual void rw_range_sett::get_objects_rec
inlineprotected

Definition at line 243 of file goto_rw.h.

◆ get_objects_rec() [2/7]

virtual void rw_range_sett::get_objects_rec
inlineprotected

Definition at line 234 of file goto_rw.h.

◆ get_objects_rec() [3/7]

void rw_guarded_range_set_value_sett::get_objects_rec ( const irep_idt &  _function,
goto_programt::const_targett  _target,
get_modet  mode,
const exprt &  expr 
)
inlineoverridevirtual

Reimplemented from rw_range_set_value_sett.

Definition at line 478 of file goto_rw.h.

◆ get_objects_rec() [4/7]

void rw_guarded_range_set_value_sett::get_objects_rec ( const irep_idt &  function,
goto_programt::const_targett  target,
const typet &  type 
)
inlineoverridevirtual

Reimplemented from rw_range_set_value_sett.

Definition at line 489 of file goto_rw.h.

◆ get_objects_rec() [5/7]

void rw_range_sett::get_objects_rec
protected

Definition at line 269 of file goto_rw.cpp.

◆ get_objects_rec() [6/7]

void rw_range_sett::get_objects_rec
protected

Definition at line 265 of file goto_rw.cpp.

◆ get_objects_rec() [7/7]

void rw_range_sett::get_objects_rec
protected

Definition at line 341 of file goto_rw.cpp.

◆ get_ranges()

const guarded_range_domaint& rw_guarded_range_set_value_sett::get_ranges ( const std::unique_ptr< range_domain_baset > &  ranges) const
inline

Definition at line 471 of file goto_rw.h.

Member Data Documentation

◆ guard

guardt rw_guarded_range_set_value_sett::guard
protected

Definition at line 499 of file goto_rw.h.

◆ guard_manager

guard_managert& rw_guarded_range_set_value_sett::guard_manager
protected

Definition at line 498 of file goto_rw.h.

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