CBMC
Loading...
Searching...
No Matches
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

 
 
 
 
 
 
 
 
void  output (std::ostream &out) const
 

Protected Member Functions

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Protected Attributes

 
 
 
 

Detailed Description

Definition at line 205 of file goto_rw.h.

Member Typedef Documentation

◆  objectst

Definition at line 208 of file goto_rw.h.

Member Enumeration Documentation

◆  get_modet

Enumerator
LHS_W 
READ 

Definition at line 234 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_handlertmessage_handler 
)
inline

Definition at line 212 of file goto_rw.h.

Member Function Documentation

◆  add()

void rw_range_sett::add ( get_modet  mode,
const irep_idtidentifier,
const range_spectrange_start,
const range_spectrange_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 &  ,
get_modet  mode,
const exprtpointer 
)
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 exprtobject )
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_exprtexpr,
const range_spectrange_start,
const range_spectsize 
)
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 range_spectrange_start,
const range_spectsize 
)
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 range_spectrange_start,
const range_spectsize 
)
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 range_spectrange_start,
const range_spectsize 
)
protectedvirtual

Definition at line 82 of file goto_rw.cpp.

◆  get_objects_dereference()

void rw_range_sett::get_objects_dereference ( get_modet  mode,
const range_spectrange_start,
const range_spectsize 
)
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_exprtif_expr,
const range_spectrange_start,
const range_spectsize 
)
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_exprtexpr,
const range_spectrange_start,
const range_spectsize 
)
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_exprtexpr,
const range_spectrange_start,
const range_spectsize 
)
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 &  ,
const typettype 
)
inlinevirtual

◆  get_objects_rec() [2/5]

virtual void rw_range_sett::get_objects_rec ( const irep_idt &  ,
get_modet  mode,
const exprtexpr 
)
inlinevirtual

◆  get_objects_rec() [3/5]

void rw_range_sett::get_objects_rec ( const typettype )
protectedvirtual

Reimplemented in rw_range_set_value_sett, and rw_guarded_range_set_value_sett.

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 exprtexpr 
)
protectedvirtual

Reimplemented in rw_range_set_value_sett, and rw_guarded_range_set_value_sett.

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 exprtexpr,
const range_spectrange_start,
const range_spectsize 
)
protectedvirtual

Reimplemented in rw_range_set_value_sett, and rw_guarded_range_set_value_sett.

Definition at line 540 of file goto_rw.cpp.

◆  get_objects_shift()

void rw_range_sett::get_objects_shift ( get_modet  mode,
const shift_exprtshift,
const range_spectrange_start,
const range_spectsize 
)
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_exprtexpr,
const range_spectrange_start,
const range_spectsize 
)
protectedvirtual

Definition at line 366 of file goto_rw.cpp.

◆  get_objects_typecast()

void rw_range_sett::get_objects_typecast ( get_modet  mode,
const range_spectrange_start,
const range_spectsize 
)
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 217 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 228 of file goto_rw.h.

◆  get_w_set()

const objectst & rw_range_sett::get_w_set ( ) const
inline

Definition at line 222 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 263 of file goto_rw.h.

◆  ns

const namespacet& rw_range_sett::ns
protected

Definition at line 262 of file goto_rw.h.

◆  r_range_set

objectst rw_range_sett::r_range_set
protected

Definition at line 265 of file goto_rw.h.

◆  w_range_set

objectst rw_range_sett::w_range_set
protected

Definition at line 265 of file goto_rw.h.


The documentation for this class was generated from the following files:
  • /home/runner/work/cbmc/cbmc/src/analyses/goto_rw.h
  • /home/runner/work/cbmc/cbmc/src/analyses/goto_rw.cpp

AltStyle によって変換されたページ (->オリジナル) /