cprover
|
#include <rw_set.h>
Public Member Functions | |
rw_set_with_trackt (const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target) | |
~rw_set_with_trackt () | |
![]() | |
_rw_set_loct (const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target) | |
~_rw_set_loct () | |
![]() | |
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 | |
std::map< const irep_idt, const irep_idt > | dereferenced_from |
std::set< irep_idt > | set_reads |
![]() | |
entriest | r_entries |
entriest | w_entries |
Protected Member Functions | |
void | track_deref (const entryt &entry, bool read) |
void | set_track_deref () |
void | reset_track_deref () |
![]() | |
void | read (const exprt &expr) |
void | read (const exprt &expr, const guardt &guard) |
void | write (const exprt &expr) |
void | compute () |
void | assign (const exprt &lhs, const exprt &rhs) |
void | read_write_rec (const exprt &expr, bool r, bool w, const std::string &suffix, const guardt &guard) |
![]() | |
virtual void | track_deref (const entryt &entry, bool read) |
Protected Attributes | |
bool | dereferencing |
std::vector< entryt > | dereferenced |
![]() | |
value_setst & | value_sets |
const goto_programt::const_targett | target |
![]() | |
const namespacet & | ns |
Additional Inherited Members | |
![]() | |
typedef std::unordered_map< irep_idt, entryt, irep_id_hash > | entriest |
|
inline |
Definition at line 249 of file rw_set.h.
References _rw_set_loct::compute().
|
inlineprotectedvirtual |
Reimplemented from rw_set_baset.
Definition at line 285 of file rw_set.h.
References dereferenced, and dereferencing.
|
inlineprotectedvirtual |
|
inlineprotected |
Definition at line 267 of file rw_set.h.
References dereferenced, dereferenced_from, dereferencing, _rw_set_loct::read(), and set_reads.
|
protected |
Definition at line 265 of file rw_set.h.
Referenced by reset_track_deref(), and track_deref().
Definition at line 235 of file rw_set.h.
Referenced by fence_all_sharedt::compute(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), and track_deref().
|
protected |
Definition at line 264 of file rw_set.h.
Referenced by reset_track_deref(), set_track_deref(), and track_deref().
std::set<irep_idt> rw_set_with_trackt::set_reads |
Definition at line 238 of file rw_set.h.
Referenced by fence_all_sharedt::compute(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), and track_deref().