#include <rw_set.h>

Inheritance diagram for rw_set_with_trackt:

Collaboration diagram for rw_set_with_trackt:

Public Member Functions
	rw_set_with_trackt (const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)

Public Member Functions inherited from _rw_set_loct
	_rw_set_loct (const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)

Public Member Functions inherited from rw_set_baset
	rw_set_baset (const namespacet &_ns)

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

Public Attributes
std::map< const irep_idt, const irep_idt >	dereferenced_from

std::set< irep_idt >	set_reads

Public Attributes inherited from rw_set_baset
entriest	r_entries

entriest	w_entries

Protected Member Functions
void	track_deref (const entryt &entry, bool read)

void	set_track_deref ()

void	reset_track_deref ()

Protected Member Functions inherited from _rw_set_loct
void	read (const exprt &expr)

void	read (const exprt &expr, const guardt &guard)

void	write (const exprt &expr)

void	compute ()

void	assign (const exprt &lhs, const exprt &rhs)

void	read_write_rec (const exprt &expr, bool r, bool w, const std::string &suffix, const guardt &guard)

Protected Member Functions inherited from rw_set_baset
virtual void	track_deref (const entryt &, bool read)

Protected Attributes
bool	dereferencing

std::vector< entryt >	dereferenced

Protected Attributes inherited from _rw_set_loct
value_setst &	value_sets

const goto_programt::const_targett	target

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 >	entriest

Detailed Description

Definition at line 222 of file rw_set.h.

Constructor & Destructor Documentation

◆ rw_set_with_trackt()

rw_set_with_trackt::rw_set_with_trackt	(	const namespacet &	_ns,
		value_setst &	_value_sets,
		goto_programt::const_targett	_target
	)

inline

Definition at line 244 of file rw_set.h.

References _rw_set_loct::compute().

Member Function Documentation

◆ reset_track_deref()

void rw_set_with_trackt::reset_track_deref ( )

inlineprotectedvirtual

Reimplemented from rw_set_baset.

Definition at line 278 of file rw_set.h.

References dereferenced, and dereferencing.

◆ set_track_deref()

void rw_set_with_trackt::set_track_deref ( )

inlineprotectedvirtual

Reimplemented from rw_set_baset.

Definition at line 273 of file rw_set.h.

References dereferencing.

◆ track_deref()

void rw_set_with_trackt::track_deref	(	const entryt &	entry,
		bool	read
	)

inlineprotected

Definition at line 260 of file rw_set.h.

References dereferenced, dereferenced_from, dereferencing, _rw_set_loct::read(), and set_reads.

Member Data Documentation

◆ dereferenced

std::vector<entryt> rw_set_with_trackt::dereferenced

protected

Definition at line 258 of file rw_set.h.

Referenced by reset_track_deref(), and track_deref().

◆ dereferenced_from

std::map<const irep_idt, const irep_idt> rw_set_with_trackt::dereferenced_from

Definition at line 230 of file rw_set.h.

Referenced by track_deref().

◆ dereferencing

bool rw_set_with_trackt::dereferencing

protected

Definition at line 257 of file rw_set.h.

Referenced by reset_track_deref(), set_track_deref(), and track_deref().

◆ set_reads

std::set<irep_idt> rw_set_with_trackt::set_reads

Definition at line 233 of file rw_set.h.

Referenced by track_deref().

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

goto-instrument/rw_set.h

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Additional Inherited Members