cprover
|
#include <rw_set.h>
Public Member Functions | |
rw_set_functiont (value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function) | |
~rw_set_functiont () | |
![]() | |
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 |
Protected Member Functions | |
void | compute_rec (const exprt &function) |
![]() | |
virtual void | track_deref (const entryt &entry, bool read) |
virtual void | set_track_deref () |
virtual void | reset_track_deref () |
Protected Attributes | |
const namespacet | ns |
value_setst & | value_sets |
const goto_functionst & | goto_functions |
![]() | |
const namespacet & | ns |
Additional Inherited Members | |
![]() | |
typedef std::unordered_map< irep_idt, entryt > | entriest |
![]() | |
entriest | r_entries |
entriest | w_entries |
|
inline |
Definition at line 204 of file rw_set.h.
References compute_rec().
|
protected |
Definition at line 198 of file rw_set.cpp.
References forall_goto_program_instructions, goto_functionst::function_map, symbol_exprt::get_identifier(), goto_functions, ns, to_if_expr(), to_symbol_expr(), and value_sets.
Referenced by rw_set_functiont().
|
protected |
Definition at line 221 of file rw_set.h.
Referenced by compute_rec().
|
protected |
Definition at line 219 of file rw_set.h.
Referenced by compute_rec().
|
protected |
Definition at line 220 of file rw_set.h.
Referenced by compute_rec().