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

#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, const irep_idt &_function_id, goto_programt::const_targett _target, message_handlert &message_handler)
Public Member Functions inherited from _rw_set_loct
 _rw_set_loct (const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target, 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

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 exprt::operandst &guard_conjuncts)
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 exprt::operandst &guard_conjuncts)

Protected Attributes

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

Detailed Description

Definition at line 240 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,
const irep_idt & _function_id,
goto_programt::const_targett _target,
message_handlert & message_handler )
inline

Definition at line 270 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 306 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 301 of file rw_set.h.

◆ track_deref()

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

Reimplemented from rw_set_baset.

Definition at line 288 of file rw_set.h.

Member Data Documentation

◆ dereferenced

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

Definition at line 286 of file rw_set.h.

◆ dereferenced_from

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

Definition at line 248 of file rw_set.h.

◆ dereferencing

bool rw_set_with_trackt::dereferencing
protected

Definition at line 285 of file rw_set.h.

◆ set_reads

std::set<irep_idt> rw_set_with_trackt::set_reads

Definition at line 251 of file rw_set.h.


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