cprover
|
Represents a set of expressions (exprt
instances) with corresponding offsets (offsett
instances).
More...
#include <value_set.h>
Public Types | |
typedef data_typet::iterator | iterator |
typedef data_typet::const_iterator | const_iterator |
typedef data_typet::value_type | value_type |
typedef data_typet::key_type | key_type |
Public Member Functions | |
iterator | begin () |
const_iterator | begin () const |
const_iterator | cbegin () const |
iterator | end () |
const_iterator | end () const |
const_iterator | cend () const |
size_t | size () const |
bool | empty () const |
void | erase (key_type i) |
void | erase (const_iterator it) |
offsett & | operator[] (key_type i) |
offsett & | at (key_type i) |
const offsett & | at (key_type i) const |
template<typename It > | |
void | insert (It b, It e) |
template<typename T > | |
const_iterator | find (T &&t) const |
object_map_dt ()=default | |
bool | operator== (const object_map_dt &other) const |
bool | operator!= (const object_map_dt &other) const |
Static Public Attributes | |
static const object_map_dt | blank {} |
Protected Member Functions | |
~object_map_dt ()=default | |
Private Types | |
typedef std::map< object_numberingt::number_type, offsett > | data_typet |
Private Attributes | |
data_typet | data |
Represents a set of expressions (exprt
instances) with corresponding offsets (offsett
instances).
This is the RHS set of a single row of the enclosing value_sett
, such as { null, dynamic_object1 }
. The set is represented as a map from numbered exprt
s to offsett
instead of a set of pairs to make lookup by exprt
easier. All methods matching the interface of std::map
forward those methods to the internal map.
Definition at line 78 of file value_set.h.
typedef data_typet::const_iterator value_sett::object_map_dt::const_iterator |
Definition at line 87 of file value_set.h.
|
private |
Definition at line 80 of file value_set.h.
typedef data_typet::iterator value_sett::object_map_dt::iterator |
Definition at line 85 of file value_set.h.
typedef data_typet::key_type value_sett::object_map_dt::key_type |
Definition at line 91 of file value_set.h.
typedef data_typet::value_type value_sett::object_map_dt::value_type |
Definition at line 89 of file value_set.h.
|
default |
|
protecteddefault |
Definition at line 111 of file value_set.h.
Definition at line 115 of file value_set.h.
|
inline |
Definition at line 93 of file value_set.h.
Referenced by value_sett::assign_rec(), value_sett::do_free(), value_sett::eval_pointer_offset(), value_sett::get_reference_set(), value_sett::get_reference_set_rec(), value_sett::get_value_set(), value_sett::get_value_set_rec(), value_sett::make_union(), and value_sett::output().
|
inline |
Definition at line 94 of file value_set.h.
|
inline |
Definition at line 95 of file value_set.h.
|
inline |
Definition at line 99 of file value_set.h.
|
inline |
Definition at line 102 of file value_set.h.
Referenced by value_sett::get_value_set_rec().
|
inline |
Definition at line 97 of file value_set.h.
Referenced by value_sett::assign_rec(), value_sett::do_free(), value_sett::eval_pointer_offset(), value_sett::get_reference_set(), value_sett::get_reference_set_rec(), value_sett::get_value_set(), value_sett::get_value_set_rec(), value_sett::insert(), value_sett::make_union(), and value_sett::output().
|
inline |
Definition at line 98 of file value_set.h.
|
inline |
Definition at line 104 of file value_set.h.
|
inline |
Definition at line 105 of file value_set.h.
|
inline |
Definition at line 124 of file value_set.h.
Referenced by value_sett::insert().
|
inline |
Definition at line 121 of file value_set.h.
Referenced by value_sett::get_value_set_rec().
|
inline |
Definition at line 134 of file value_set.h.
|
inline |
Definition at line 130 of file value_set.h.
References data.
Definition at line 107 of file value_set.h.
|
inline |
Definition at line 101 of file value_set.h.
References data::size.
Referenced by value_sett::assign_rec(), and value_sett::get_value_set_rec().
|
static |
Definition at line 126 of file value_set.h.
|
private |
Definition at line 81 of file value_set.h.
Referenced by operator==().