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

Protected Attributes
value_setst &	value_sets
const goto_functionst &	goto_functions
Protected Attributes inherited from rw_set_baset
const namespacet &	ns

Additional Inherited Members
Public Types inherited from rw_set_baset
typedef std::unordered_map< irep_idt, entryt, irep_id_hash >	entriest
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

Definition at line 198 of file rw_set.cpp.

References forall_goto_program_instructions, goto_functions_templatet< bodyT >::function_map, symbol_exprt::get_identifier(), goto_functions, rw_set_baset::ns, to_if_expr(), to_symbol_expr(), and value_sets.

Referenced by rw_set_functiont().

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:

• goto-instrument/rw_set.h
• goto-instrument/rw_set.cpp