cprover
rw_set_functiont Class Reference

#include <rw_set.h>

Inheritance diagram for rw_set_functiont:
[legend]
Collaboration diagram for rw_set_functiont:
[legend]

Public Member Functions

 rw_set_functiont (value_setst &_value_sets, const namespacet &_ns, const goto_functionst &_goto_functions, const exprt &function)
 
 ~rw_set_functiont ()
 
- Public Member Functions inherited from rw_set_baset
 rw_set_baset (const namespacet &_ns)
 
 ~rw_set_baset ()
 
void swap (rw_set_baset &other)
 
rw_set_basetoperator+= (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 &entry, bool read)
 
virtual void set_track_deref ()
 
virtual void reset_track_deref ()
 

Protected Attributes

value_setstvalue_sets
 
const goto_functionstgoto_functions
 
- Protected Attributes inherited from rw_set_baset
const namespacetns
 

Additional Inherited Members

- Public Types inherited from rw_set_baset
typedef std::unordered_map< irep_idt, entryt, irep_id_hashentriest
 
- Public Attributes inherited from rw_set_baset
entriest r_entries
 
entriest w_entries
 

Detailed Description

Definition at line 201 of file rw_set.h.

Constructor & Destructor Documentation

◆ rw_set_functiont()

rw_set_functiont::rw_set_functiont ( value_setst _value_sets,
const namespacet _ns,
const goto_functionst _goto_functions,
const exprt function 
)
inline

Definition at line 204 of file rw_set.h.

References compute_rec().

◆ ~rw_set_functiont()

rw_set_functiont::~rw_set_functiont ( )
inline

Definition at line 216 of file rw_set.h.

Member Function Documentation

◆ compute_rec()

void rw_set_functiont::compute_rec ( const exprt function)
protected

Member Data Documentation

◆ goto_functions

const goto_functionst& rw_set_functiont::goto_functions
protected

Definition at line 220 of file rw_set.h.

Referenced by compute_rec().

◆ value_sets

value_setst& rw_set_functiont::value_sets
protected

Definition at line 219 of file rw_set.h.

Referenced by compute_rec().


The documentation for this class was generated from the following files: