CBMC
|
#include <rw_set.h>
Public Member Functions | |
rw_set_with_trackt (const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler) | |
Public Member Functions inherited from _rw_set_loct | |
_rw_set_loct (const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler) | |
Public Member Functions inherited from rw_set_baset | |
rw_set_baset (const namespacet &_ns, message_handlert &message_handler) | |
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 |
Public Attributes inherited from rw_set_baset | |
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 () |
Protected Member Functions inherited from _rw_set_loct | |
void | read (const exprt &expr) |
void | read (const exprt &expr, const exprt::operandst &guard_conjuncts) |
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 exprt::operandst &guard_conjuncts) |
Protected Attributes | |
bool | dereferencing |
std::vector< entryt > | dereferenced |
Protected Attributes inherited from _rw_set_loct | |
value_setst & | value_sets |
const irep_idt | function_id |
const goto_programt::const_targett | target |
Protected Attributes inherited from rw_set_baset | |
const namespacet & | ns |
message_handlert & | message_handler |
Additional Inherited Members | |
Public Types inherited from rw_set_baset | |
typedef std::unordered_map< irep_idt, entryt > | entriest |
|
inline |
|
inlineprotectedvirtual |
Reimplemented from rw_set_baset.
|
inlineprotectedvirtual |
Reimplemented from rw_set_baset.
|
inlineprotectedvirtual |
Reimplemented from rw_set_baset.
|
protected |