cprover
rw_set_baset Class Reference

#include <rw_set.h>

Inheritance diagram for rw_set_baset:
[legend]
Collaboration diagram for rw_set_baset:
[legend]

Classes

struct  entryt
 

Public Types

typedef std::unordered_map< irep_idt, entrytentriest
 

Public Member Functions

 rw_set_baset (const namespacet &_ns)
 
 ~rw_set_baset ()
 
void swap (rw_set_baset &other)
 
rw_set_basetoperator+= (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 &entry, bool read)
 
virtual void set_track_deref ()
 
virtual void reset_track_deref ()
 

Protected Attributes

const namespacetns
 

Detailed Description

Definition at line 35 of file rw_set.h.

Member Typedef Documentation

◆ entriest

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

Definition at line 56 of file rw_set.h.

Constructor & Destructor Documentation

◆ rw_set_baset()

rw_set_baset::rw_set_baset ( const namespacet _ns)
inlineexplicit

Definition at line 38 of file rw_set.h.

◆ ~rw_set_baset()

rw_set_baset::~rw_set_baset ( )
inline

Definition at line 43 of file rw_set.h.

Member Function Documentation

◆ empty()

bool rw_set_baset::empty ( ) const
inline

Definition at line 72 of file rw_set.h.

References r_entries, and w_entries.

Referenced by introduce_temporaries(), mmio(), and shared_bufferst::cfg_visitort::weak_memory().

◆ has_r_entry()

bool rw_set_baset::has_r_entry ( irep_idt  object) const
inline

Definition at line 82 of file rw_set.h.

References r_entries.

Referenced by potential_race_on_write().

◆ has_w_entry()

bool rw_set_baset::has_w_entry ( irep_idt  object) const
inline

Definition at line 77 of file rw_set.h.

References w_entries.

Referenced by potential_race_on_read(), and potential_race_on_write().

◆ operator+=()

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

Definition at line 65 of file rw_set.h.

References r_entries, and w_entries.

◆ output()

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

Definition at line 24 of file rw_set.cpp.

References from_expr(), ns, r_entries, and w_entries.

Referenced by operator<<().

◆ reset_track_deref()

virtual void rw_set_baset::reset_track_deref ( )
inlineprotectedvirtual

Reimplemented in rw_set_with_trackt.

Definition at line 92 of file rw_set.h.

Referenced by _rw_set_loct::read_write_rec().

◆ set_track_deref()

virtual void rw_set_baset::set_track_deref ( )
inlineprotectedvirtual

Reimplemented in rw_set_with_trackt.

Definition at line 91 of file rw_set.h.

Referenced by _rw_set_loct::read_write_rec().

◆ swap()

void rw_set_baset::swap ( rw_set_baset other)
inline

Definition at line 59 of file rw_set.h.

References r_entries, and w_entries.

◆ track_deref()

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

Definition at line 90 of file rw_set.h.

Referenced by _rw_set_loct::read_write_rec().

Member Data Documentation

◆ ns

const namespacet& rw_set_baset::ns
protected

Definition at line 94 of file rw_set.h.

Referenced by output(), and _rw_set_loct::read_write_rec().

◆ r_entries

◆ w_entries


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