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

#include <rw_set.h>

+ Inheritance diagram for rw_set_baset:
+ Collaboration diagram for rw_set_baset:

Classes

struct  entryt
 

Public Types

typedef std::unordered_map< irep_idt, entryt > entriest
 

Public Member Functions

 rw_set_baset (const namespacet &_ns, message_handlert &message_handler)
 
virtual ~rw_set_baset ()=default
 
void swap (rw_set_baset &other)
 
rw_set_baset & operator+= (const rw_set_baset &other)
 
bool empty () const
 
bool has_w_entry (irep_idt object) const
 
bool has_r_entry (irep_idt object) const
 
void output (std::ostream &out) const
 

Public Attributes

entriest r_entries
 
entriest w_entries
 

Protected Member Functions

virtual void track_deref (const entryt &, bool read)
 
virtual void set_track_deref ()
 
virtual void reset_track_deref ()
 

Protected Attributes

const namespacet & ns
 
message_handlert & message_handler
 

Detailed Description

Definition at line 34 of file rw_set.h.

Member Typedef Documentation

◆ entriest

typedef std::unordered_map<irep_idt, entryt> rw_set_baset::entriest

Definition at line 59 of file rw_set.h.

Constructor & Destructor Documentation

◆ rw_set_baset()

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

Definition at line 37 of file rw_set.h.

◆ ~rw_set_baset()

virtual rw_set_baset::~rw_set_baset ( )
virtualdefault

Member Function Documentation

◆ empty()

bool rw_set_baset::empty ( ) const
inline

Definition at line 75 of file rw_set.h.

◆ has_r_entry()

bool rw_set_baset::has_r_entry ( irep_idt  object) const
inline

Definition at line 85 of file rw_set.h.

◆ has_w_entry()

bool rw_set_baset::has_w_entry ( irep_idt  object) const
inline

Definition at line 80 of file rw_set.h.

◆ operator+=()

rw_set_baset& rw_set_baset::operator+= ( const rw_set_baset &  other)
inline

Definition at line 68 of file rw_set.h.

◆ output()

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

Definition at line 22 of file rw_set.cpp.

◆ reset_track_deref()

virtual void rw_set_baset::reset_track_deref ( )
inlineprotectedvirtual

Reimplemented in rw_set_with_trackt.

Definition at line 98 of file rw_set.h.

◆ set_track_deref()

virtual void rw_set_baset::set_track_deref ( )
inlineprotectedvirtual

Reimplemented in rw_set_with_trackt.

Definition at line 97 of file rw_set.h.

◆ swap()

void rw_set_baset::swap ( rw_set_baset &  other)
inline

Definition at line 62 of file rw_set.h.

◆ track_deref()

virtual void rw_set_baset::track_deref ( const entryt &  ,
bool  read 
)
inlineprotectedvirtual

Reimplemented in rw_set_with_trackt.

Definition at line 93 of file rw_set.h.

Member Data Documentation

◆ message_handler

message_handlert& rw_set_baset::message_handler
protected

Definition at line 101 of file rw_set.h.

◆ ns

const namespacet& rw_set_baset::ns
protected

Definition at line 100 of file rw_set.h.

◆ r_entries

entriest rw_set_baset::r_entries

Definition at line 60 of file rw_set.h.

◆ w_entries

entriest rw_set_baset::w_entries

Definition at line 60 of file rw_set.h.

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