cprover
|
#include <rw_set.h>
Classes | |
struct | entryt |
Public Types | |
typedef std::unordered_map< irep_idt, entryt, irep_id_hash > | entriest |
Public Member Functions | |
rw_set_baset (const namespacet &_ns) | |
~rw_set_baset () | |
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 &entry, bool read) |
virtual void | set_track_deref () |
virtual void | reset_track_deref () |
Protected Attributes | |
const namespacet & | ns |
typedef std::unordered_map<irep_idt, entryt, irep_id_hash> rw_set_baset::entriest |
|
inlineexplicit |
|
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().
|
inline |
Definition at line 82 of file rw_set.h.
References r_entries.
Referenced by potential_race_on_write().
|
inline |
Definition at line 77 of file rw_set.h.
References w_entries.
Referenced by potential_race_on_read(), and potential_race_on_write().
|
inline |
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<<().
|
inlineprotectedvirtual |
Reimplemented in rw_set_with_trackt.
Definition at line 92 of file rw_set.h.
Referenced by _rw_set_loct::read_write_rec().
|
inlineprotectedvirtual |
Reimplemented in rw_set_with_trackt.
Definition at line 91 of file rw_set.h.
Referenced by _rw_set_loct::read_write_rec().
|
inline |
|
inlineprotectedvirtual |
Definition at line 90 of file rw_set.h.
Referenced by _rw_set_loct::read_write_rec().
|
protected |
Definition at line 94 of file rw_set.h.
Referenced by rw_set_functiont::compute_rec(), output(), and _rw_set_loct::read_write_rec().
entriest rw_set_baset::r_entries |
Definition at line 57 of file rw_set.h.
Referenced by fence_all_sharedt::compute(), instrumentert::cfg_visitort::contains_shared_array(), empty(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), has_r_entry(), has_shared_entries(), operator+=(), output(), _rw_set_loct::read_write_rec(), and swap().
entriest rw_set_baset::w_entries |
Definition at line 57 of file rw_set.h.
Referenced by fence_all_sharedt::compute(), instrumentert::cfg_visitort::contains_shared_array(), empty(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), has_shared_entries(), has_w_entry(), operator+=(), output(), _rw_set_loct::read_write_rec(), and swap().