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_loct (const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target) | |
![]() | |
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 | |
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 &, 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 > | entriest |
|
inline |
Definition at line 244 of file rw_set.h.
References _rw_set_loct::compute().
|
inlineprotectedvirtual |
Reimplemented from rw_set_baset.
Definition at line 278 of file rw_set.h.
References dereferenced, and dereferencing.
|
inlineprotectedvirtual |
|
inlineprotected |
Definition at line 260 of file rw_set.h.
References dereferenced, dereferenced_from, dereferencing, _rw_set_loct::read(), and set_reads.
|
protected |
Definition at line 258 of file rw_set.h.
Referenced by reset_track_deref(), and track_deref().
Definition at line 230 of file rw_set.h.
Referenced by track_deref().
|
protected |
Definition at line 257 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 233 of file rw_set.h.
Referenced by track_deref().