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

Detailed Description

Definition at line 33 of file rw_set.h.

Member Typedef Documentation

entriest

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

Definition at line 58 of file rw_set.h.

Constructor & Destructor Documentation

rw_set_baset()

rw_set_baset::rw_set_baset ( const namespacet &  _ns )

inlineexplicit

Definition at line 36 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 74 of file rw_set.h.

has_r_entry()

bool rw_set_baset::has_r_entry ( irep_idt  object ) const

inline

Definition at line 84 of file rw_set.h.

has_w_entry()

bool rw_set_baset::has_w_entry ( irep_idt  object ) const

inline

Definition at line 79 of file rw_set.h.

operator+=()

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

inline

Definition at line 67 of file rw_set.h.

output()

void rw_set_baset::output

(

std::ostream &

out

)

const

Definition at line 23 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 97 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 96 of file rw_set.h.

swap()

void rw_set_baset::swap ( rw_set_baset &  other )

inline

Definition at line 61 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 92 of file rw_set.h.

Member Data Documentation

ns

const namespacet& rw_set_baset::ns

protected

Definition at line 99 of file rw_set.h.

r_entries

entriest rw_set_baset::r_entries

Definition at line 59 of file rw_set.h.

w_entries

entriest rw_set_baset::w_entries

Definition at line 59 of file rw_set.h.

---

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

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