CBMC
range_domaint Class Reference

#include <goto_rw.h>

+ Inheritance diagram for range_domaint:
+ Collaboration diagram for range_domaint:

Public Types

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

Public Member Functions

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
 
void push_back (const sub_typet::value_type &v)
 
void push_back (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::list< std::pair< range_spect, range_spect > > sub_typet
 

Private Attributes

sub_typet data
 

Detailed Description

Definition at line 174 of file goto_rw.h.

Member Typedef Documentation

◆ const_iterator

typedef sub_typet::const_iterator range_domaint::const_iterator

Definition at line 185 of file goto_rw.h.

◆ iterator

typedef sub_typet::iterator range_domaint::iterator

Definition at line 183 of file goto_rw.h.

◆ sub_typet

typedef std::list<std::pair<range_spect, range_spect> > range_domaint::sub_typet
private

Definition at line 176 of file goto_rw.h.

Member Function Documentation

◆ begin() [1/2]

iterator range_domaint::begin ( )
inline

Definition at line 187 of file goto_rw.h.

◆ begin() [2/2]

const_iterator range_domaint::begin ( ) const
inline

Definition at line 188 of file goto_rw.h.

◆ cbegin()

const_iterator range_domaint::cbegin ( ) const
inline

Definition at line 189 of file goto_rw.h.

◆ cend()

const_iterator range_domaint::cend ( ) const
inline

Definition at line 193 of file goto_rw.h.

◆ end() [1/2]

iterator range_domaint::end ( )
inline

Definition at line 191 of file goto_rw.h.

◆ end() [2/2]

const_iterator range_domaint::end ( ) const
inline

Definition at line 192 of file goto_rw.h.

◆ output()

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

Implements range_domain_baset.

Definition at line 34 of file goto_rw.cpp.

◆ push_back() [1/2]

void range_domaint::push_back ( const sub_typet::value_type &  v)
inline

Definition at line 195 of file goto_rw.h.

◆ push_back() [2/2]

void range_domaint::push_back ( sub_typet::value_type &&  v)
inline

Definition at line 196 of file goto_rw.h.

Member Data Documentation

◆ data

sub_typet range_domaint::data
private

Definition at line 177 of file goto_rw.h.


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