CBMC
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: