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

#include <goto_rw.h>

Inheritance diagram for guarded_range_domaint:
Collaboration diagram for guarded_range_domaint:

Public Types

typedef sub_typet::iterator iterator
typedef sub_typet::const_iterator const_iterator

Public Member Functions

virtual void output (const namespacet &ns, std::ostream &out) const override
iterator begin ()
const_iterator begin () const
const_iterator cbegin () const
iterator end ()
const_iterator end () const
const_iterator cend () const
iterator insert (const sub_typet::value_type &v)
iterator insert (sub_typet::value_type &&v)
Public Member Functions inherited from range_domain_baset
 range_domain_baset ()=default
 range_domain_baset (const range_domain_baset &rhs)=delete
range_domain_basetoperator= (const range_domain_baset &rhs)=delete
 range_domain_baset (range_domain_baset &&rhs)=delete
range_domain_basetoperator= (range_domain_baset &&rhs)=delete
virtual ~range_domain_baset ()

Private Types

typedef std::multimap< range_spect, std::pair< range_spect, exprt > > sub_typet

Private Attributes

sub_typet data

Detailed Description

Definition at line 424 of file goto_rw.h.

Member Typedef Documentation

◆ const_iterator

typedef sub_typet::const_iterator guarded_range_domaint::const_iterator

Definition at line 435 of file goto_rw.h.

◆ iterator

typedef sub_typet::iterator guarded_range_domaint::iterator

Definition at line 433 of file goto_rw.h.

◆ sub_typet

typedef std::multimap<range_spect, std::pair<range_spect, exprt> > guarded_range_domaint::sub_typet
private

Definition at line 426 of file goto_rw.h.

Member Function Documentation

◆ begin() [1/2]

iterator guarded_range_domaint::begin ( )
inline

Definition at line 437 of file goto_rw.h.

◆ begin() [2/2]

const_iterator guarded_range_domaint::begin ( ) const
inline

Definition at line 438 of file goto_rw.h.

◆ cbegin()

const_iterator guarded_range_domaint::cbegin ( ) const
inline

Definition at line 439 of file goto_rw.h.

◆ cend()

const_iterator guarded_range_domaint::cend ( ) const
inline

Definition at line 443 of file goto_rw.h.

◆ end() [1/2]

iterator guarded_range_domaint::end ( )
inline

Definition at line 441 of file goto_rw.h.

◆ end() [2/2]

const_iterator guarded_range_domaint::end ( ) const
inline

Definition at line 442 of file goto_rw.h.

◆ insert() [1/2]

iterator guarded_range_domaint::insert ( const sub_typet::value_type & v)
inline

Definition at line 445 of file goto_rw.h.

◆ insert() [2/2]

iterator guarded_range_domaint::insert ( sub_typet::value_type && v)
inline

Definition at line 450 of file goto_rw.h.

◆ output()

void guarded_range_domaint::output ( const namespacet & ns,
std::ostream & out ) const
overridevirtual

Implements range_domain_baset.

Definition at line 714 of file goto_rw.cpp.

Member Data Documentation

◆ data

sub_typet guarded_range_domaint::data
private

Definition at line 427 of file goto_rw.h.


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