CBMC
|
#include <goto_rw.h>
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_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::list< std::pair< range_spect, range_spect > > | sub_typet |
Private Attributes | |
sub_typet | data |
typedef sub_typet::const_iterator range_domaint::const_iterator |
typedef sub_typet::iterator range_domaint::iterator |
|
private |
|
inline |
|
inline |
|
inline |
|
inline |
|
overridevirtual |
Implements range_domain_baset.
Definition at line 34 of file goto_rw.cpp.
|
inline |
|
inline |