CBMC
Public Member Functions | List of all members
rw_set_loct Class Reference

#include <rw_set.h>

+ Inheritance diagram for rw_set_loct:
+ Collaboration diagram for rw_set_loct:

Public Member Functions

 rw_set_loct (const namespacet &_ns, value_setst &_value_sets, const irep_idt &_function_id, goto_programt::const_targett _target)
 
- 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)
 
- 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
 

Additional Inherited Members

- Public Types inherited from rw_set_baset
typedef std::unordered_map< irep_idt, entryt > entriest
 
- Public Attributes inherited from rw_set_baset
entriest r_entries
 
entriest w_entries
 
- 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 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 inherited from _rw_set_loct
value_setst & value_sets
 
const irep_idt function_id
 
const goto_programt::const_targett target
 
- Protected Attributes inherited from rw_set_baset
const namespacet & ns
 

Detailed Description

Definition at line 176 of file rw_set.h.

Constructor & Destructor Documentation

◆ rw_set_loct()

rw_set_loct::rw_set_loct ( const namespacet &  _ns,
value_setst &  _value_sets,
const irep_idt &  _function_id,
goto_programt::const_targett  _target 
)
inline

Definition at line 188 of file rw_set.h.

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