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_baset &	operator= (const range_domain_baset &rhs)=delete
	range_domain_baset (range_domain_baset &&rhs)=delete
range_domain_baset &	operator= (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 710 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:

• /home/runner/work/cbmc/cbmc/src/analyses/goto_rw.h
• /home/runner/work/cbmc/cbmc/src/analyses/goto_rw.cpp