CBMC
|
#include <rw_set.h>
Public Member Functions | |
rw_set_functiont (value_setst &_value_sets, const goto_modelt &_goto_model, const exprt &function, 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 |
Protected Member Functions | |
void | compute_rec (const exprt &function) |
Protected Member Functions inherited from rw_set_baset | |
virtual void | track_deref (const entryt &, 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 |
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 |
Public Attributes inherited from rw_set_baset | |
entriest | r_entries |
entriest | w_entries |
|
inline |
|
protected |
Definition at line 193 of file rw_set.cpp.
|
protected |
|
protected |
|
protected |