cprover
Loading...
Searching...
No Matches
rw_set_functiont Class Reference

#include <rw_set.h>

Inheritance diagram for rw_set_functiont:
Collaboration diagram for rw_set_functiont:

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_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 &, bool read)
virtual void set_track_deref ()
virtual void reset_track_deref ()

Protected Attributes

const namespacet ns
value_setstvalue_sets
const goto_functionstgoto_functions
Protected Attributes inherited from rw_set_baset
const namespacetns
message_handlertmessage_handler

Additional Inherited Members

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

Detailed Description

Definition at line 214 of file rw_set.h.

Constructor & Destructor Documentation

◆ rw_set_functiont()

rw_set_functiont::rw_set_functiont ( value_setst & _value_sets,
const goto_modelt & _goto_model,
const exprt & function,
message_handlert & message_handler )
inline

Definition at line 217 of file rw_set.h.

Member Function Documentation

◆ compute_rec()

void rw_set_functiont::compute_rec ( const exprt & function)
protected

Definition at line 193 of file rw_set.cpp.

Member Data Documentation

◆ goto_functions

const goto_functionst& rw_set_functiont::goto_functions
protected

Definition at line 233 of file rw_set.h.

◆ ns

const namespacet rw_set_functiont::ns
protected

Definition at line 231 of file rw_set.h.

◆ value_sets

value_setst& rw_set_functiont::value_sets
protected

Definition at line 232 of file rw_set.h.


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