Loading...

Searching...

No Matches

rw_set_baset Class Reference

#include <rw_set.h>

+ Inheritance diagram for rw_set_baset:

[フレーム]

[legend]

+ Collaboration diagram for rw_set_baset:

[フレーム]

[legend]

Classes

struct entryt

Public Types

typedef std::unordered_map< irep_idt, entryt > entriest

Public Member Functions

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

Public Attributes

entriest r_entries

entriest w_entries

Protected Member Functions

virtual void track_deref (const entryt &, bool read)

virtual void set_track_deref ()

virtual void reset_track_deref ()

Protected Attributes

const namespacet & ns

message_handlert & message_handler

Detailed Description

Definition at line 34 of file rw_set.h.

Member Typedef Documentation

◆ entriest

typedef std::unordered_map<irep_idt, entryt> rw_set_baset::entriest

Definition at line 59 of file rw_set.h.

Constructor & Destructor Documentation

◆ rw_set_baset()

rw_set_baset::rw_set_baset ( const namespacet & _ns,

message_handlert & message_handler

)

inline

Definition at line 37 of file rw_set.h.

◆ ~rw_set_baset()

virtual rw_set_baset::~rw_set_baset ( )

virtualdefault

Member Function Documentation

◆ empty()

bool rw_set_baset::empty ( ) const

inline

Definition at line 75 of file rw_set.h.

◆ has_r_entry()

bool rw_set_baset::has_r_entry ( irep_idt object ) const

inline

Definition at line 85 of file rw_set.h.

◆ has_w_entry()

bool rw_set_baset::has_w_entry ( irep_idt object ) const

inline

Definition at line 80 of file rw_set.h.

◆ operator+=()

rw_set_baset & rw_set_baset::operator+= ( const rw_set_baset & other )

inline

Definition at line 68 of file rw_set.h.

◆ output()

void rw_set_baset::output ( std::ostream & out ) const

Definition at line 22 of file rw_set.cpp.

◆ reset_track_deref()

virtual void rw_set_baset::reset_track_deref ( )

inlineprotectedvirtual

Reimplemented in rw_set_with_trackt.

Definition at line 98 of file rw_set.h.

◆ set_track_deref()

virtual void rw_set_baset::set_track_deref ( )

inlineprotectedvirtual

Reimplemented in rw_set_with_trackt.

Definition at line 97 of file rw_set.h.

◆ swap()

void rw_set_baset::swap ( rw_set_baset & other )

inline

Definition at line 62 of file rw_set.h.

◆ track_deref()

virtual void rw_set_baset::track_deref ( const entryt & ,

bool read

)

inlineprotectedvirtual

Reimplemented in rw_set_with_trackt.

Definition at line 93 of file rw_set.h.

Member Data Documentation

◆ message_handler

message_handlert& rw_set_baset::message_handler

protected

Definition at line 101 of file rw_set.h.

◆ ns

const namespacet& rw_set_baset::ns

protected

Definition at line 100 of file rw_set.h.

◆ r_entries

entriest rw_set_baset::r_entries

Definition at line 60 of file rw_set.h.

◆ w_entries

entriest rw_set_baset::w_entries

Definition at line 60 of file rw_set.h.

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

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