cprover
Loading...
Searching...
No Matches
_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, 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

Protected Member Functions

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

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
Public Attributes inherited from rw_set_baset
entriest r_entries
entriest w_entries

Detailed Description

Definition at line 113 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,
message_handlert & message_handler )
inline

Definition at line 130 of file rw_set.h.

Member Function Documentation

◆ assign()

void _rw_set_loct::assign ( const exprt & lhs,
const exprt & rhs )
protected

Definition at line 73 of file rw_set.cpp.

◆ compute()

void _rw_set_loct::compute ( )
protected

Definition at line 45 of file rw_set.cpp.

◆ read() [1/2]

void _rw_set_loct::read ( const exprt & expr)
inlineprotected

Definition at line 153 of file rw_set.h.

◆ read() [2/2]

void _rw_set_loct::read ( const exprt & expr,
const exprt::operandst & guard_conjuncts )
inlineprotected

Definition at line 158 of file rw_set.h.

◆ read_write_rec()

void _rw_set_loct::read_write_rec ( const exprt & expr,
bool r,
bool w,
const std::string & suffix,
const exprt::operandst & guard_conjuncts )
protected

Definition at line 79 of file rw_set.cpp.

◆ write()

void _rw_set_loct::write ( const exprt & expr)
inlineprotected

Definition at line 163 of file rw_set.h.

Member Data Documentation

◆ function_id

const irep_idt _rw_set_loct::function_id
protected

Definition at line 146 of file rw_set.h.

◆ target

const goto_programt::const_targett _rw_set_loct::target
protected

Definition at line 147 of file rw_set.h.

◆ value_sets

value_setst& _rw_set_loct::value_sets
protected

Definition at line 145 of file rw_set.h.


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