Loading...

Searching...

No Matches

Public Member Functions | List of all members

rw_set_loct Class Reference

#include <rw_set.h>

+ Inheritance diagram for rw_set_loct:

[フレーム]

[legend]

+ Collaboration diagram for rw_set_loct:

[フレーム]

[legend]

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

message_handlert & message_handler

Detailed Description

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

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/rw_set.h