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:

• /home/runner/work/cbmc/cbmc/src/goto-instrument/rw_set.h
• /home/runner/work/cbmc/cbmc/src/goto-instrument/rw_set.cpp