cprover
|
#include <rw_set.h>
Public Member Functions | |
_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 |
Protected Member Functions | |
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) |
virtual void | set_track_deref () |
virtual void | reset_track_deref () |
Protected Attributes | |
value_setst & | value_sets |
const goto_programt::const_targett | target |
![]() | |
const namespacet & | ns |
Additional Inherited Members | |
![]() | |
typedef std::unordered_map< irep_idt, entryt > | entriest |
![]() | |
entriest | r_entries |
entriest | w_entries |
|
inline |
Definition at line 79 of file rw_set.cpp.
References read(), and read_write_rec().
Referenced by compute().
|
protected |
Definition at line 47 of file rw_set.cpp.
References code_function_callt::arguments(), assign(), code_function_callt::function(), irept::is_not_nil(), code_function_callt::lhs(), read(), target, to_code_function_call(), and write().
Referenced by rw_set_loct::rw_set_loct(), and rw_set_with_trackt::rw_set_with_trackt().
|
inlineprotected |
Definition at line 147 of file rw_set.h.
References read_write_rec().
Referenced by assign(), compute(), read_write_rec(), and rw_set_with_trackt::track_deref().
Definition at line 152 of file rw_set.h.
References read_write_rec().
|
protected |
Definition at line 85 of file rw_set.cpp.
References guardt::as_expr(), dereference(), forall_operands, irept::get(), symbol_exprt::get_identifier(), irept::get_string(), rw_set_baset::entryt::guard, irept::id(), id2string(), rw_set_baset::ns, rw_set_baset::entryt::object, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), r, rw_set_baset::r_entries, read(), rw_set_baset::reset_track_deref(), rw_set_baset::set_track_deref(), rw_set_baset::entryt::symbol_expr, target, to_symbol_expr(), rw_set_baset::track_deref(), value_sets, and rw_set_baset::w_entries.
|
inlineprotected |
|
protected |
Definition at line 141 of file rw_set.h.
Referenced by compute(), and read_write_rec().
|
protected |
Definition at line 140 of file rw_set.h.
Referenced by read_write_rec().