cprover
rw_set_with_trackt Class Reference

#include <rw_set.h>

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

Public Member Functions

 rw_set_with_trackt (const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
 
 ~rw_set_with_trackt ()
 
- Public Member Functions inherited from _rw_set_loct
 _rw_set_loct (const namespacet &_ns, value_setst &_value_sets, goto_programt::const_targett _target)
 
 ~_rw_set_loct ()
 
- 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
 

Public Attributes

std::map< const irep_idt, const irep_idtdereferenced_from
 
std::set< irep_idtset_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 &entry, bool read)
 

Protected Attributes

bool dereferencing
 
std::vector< entryt > dereferenced
 
- Protected Attributes inherited from _rw_set_loct
value_setstvalue_sets
 
const goto_programt::const_targett target
 
- 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
 

Detailed Description

Definition at line 227 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 249 of file rw_set.h.

§ ~rw_set_with_trackt()

rw_set_with_trackt::~rw_set_with_trackt ( )
inline

Definition at line 260 of file rw_set.h.

Member Function Documentation

§ reset_track_deref()

void rw_set_with_trackt::reset_track_deref ( )
inlineprotectedvirtual

Reimplemented from rw_set_baset.

Definition at line 285 of file rw_set.h.

§ set_track_deref()

void rw_set_with_trackt::set_track_deref ( )
inlineprotectedvirtual

Reimplemented from rw_set_baset.

Definition at line 280 of file rw_set.h.

§ track_deref()

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

Definition at line 267 of file rw_set.h.

Member Data Documentation

§ dereferenced

std::vector<entryt> rw_set_with_trackt::dereferenced
protected

Definition at line 265 of file rw_set.h.

§ dereferenced_from

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

§ dereferencing

bool rw_set_with_trackt::dereferencing
protected

Definition at line 264 of file rw_set.h.

§ set_reads

std::set<irep_idt> rw_set_with_trackt::set_reads

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