CBMC
|
Depth first search iterator base - iterates over supplied expression and all its operands recursively. More...
#include <expr_iterator.h>
Public Types | |
typedef void | difference_type |
typedef exprt | value_type |
typedef const exprt * | pointer |
typedef const exprt & | reference |
typedef std::forward_iterator_tag | iterator_category |
Public Member Functions | |
template<typename other_depth_iterator_t > | |
bool | operator== (const depth_iterator_baset< other_depth_iterator_t > &other) const |
template<typename other_depth_iterator_t > | |
bool | operator!= (const depth_iterator_baset< other_depth_iterator_t > &other) const |
depth_iterator_t & | operator++ () |
Preincrement operator Do not call on the end() iterator. More... | |
depth_iterator_t & | next_sibling_or_parent () |
depth_iterator_t | operator++ (int) |
Post-increment operator Expensive copy. More... | |
const exprt & | operator* () const |
Dereference operator Dereferencing end() iterator is undefined behaviour. More... | |
const exprt * | operator-> () const |
Dereference operator (member access) Dereferencing end() iterator is undefined behaviour. More... | |
Protected Member Functions | |
depth_iterator_baset ()=default | |
Create end iterator. More... | |
depth_iterator_baset (const exprt &root) | |
Create begin iterator, starting at the supplied node. More... | |
~depth_iterator_baset ()=default | |
Destructor Protected to discourage upcasting. More... | |
depth_iterator_baset (const depth_iterator_baset &)=default | |
depth_iterator_baset (depth_iterator_baset &&other) | |
depth_iterator_baset & | operator= (const depth_iterator_baset &)=default |
depth_iterator_baset & | operator= (depth_iterator_baset &&other) |
const exprt & | get_root () |
exprt & | mutate () |
Obtain non-const exprt reference. More... | |
bool | push_expr (const exprt &expr) |
Pushes expression onto the stack If overridden, this function should be called from the inheriting class by the override function. More... | |
Private Member Functions | |
depth_iterator_t & | downcast () |
Private Attributes | |
std::deque< depth_iterator_expr_statet > | m_stack |
Friends | |
template<typename other_depth_iterator_t > | |
class | depth_iterator_baset |
Depth first search iterator base - iterates over supplied expression and all its operands recursively.
Base class using CRTP Do override .push_expr method of this class, but when doing so make this class a friend so it has access to that overridden .push_expr method in the child class
Definition at line 66 of file expr_iterator.h.
typedef void depth_iterator_baset< depth_iterator_t >::difference_type |
Definition at line 69 of file expr_iterator.h.
typedef std::forward_iterator_tag depth_iterator_baset< depth_iterator_t >::iterator_category |
Definition at line 73 of file expr_iterator.h.
typedef const exprt* depth_iterator_baset< depth_iterator_t >::pointer |
Definition at line 71 of file expr_iterator.h.
typedef const exprt& depth_iterator_baset< depth_iterator_t >::reference |
Definition at line 72 of file expr_iterator.h.
typedef exprt depth_iterator_baset< depth_iterator_t >::value_type |
Definition at line 70 of file expr_iterator.h.
|
protecteddefault |
Create end iterator.
|
inlineexplicitprotected |
Create begin iterator, starting at the supplied node.
Definition at line 155 of file expr_iterator.h.
|
protecteddefault |
Destructor Protected to discourage upcasting.
|
protecteddefault |
|
inlineprotected |
Definition at line 163 of file expr_iterator.h.
|
inlineprivate |
Definition at line 213 of file expr_iterator.h.
|
inlineprotected |
Definition at line 172 of file expr_iterator.h.
|
inlineprotected |
Obtain non-const exprt reference.
Performs a copy-on-write on the root node as a side effect.
Definition at line 182 of file expr_iterator.h.
|
inline |
Definition at line 116 of file expr_iterator.h.
|
inline |
Definition at line 86 of file expr_iterator.h.
|
inline |
Dereference operator Dereferencing end() iterator is undefined behaviour.
Definition at line 139 of file expr_iterator.h.
|
inline |
Preincrement operator Do not call on the end() iterator.
Definition at line 94 of file expr_iterator.h.
|
inline |
Post-increment operator Expensive copy.
Avoid if possible
Definition at line 130 of file expr_iterator.h.
|
inline |
Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.
Definition at line 147 of file expr_iterator.h.
|
protecteddefault |
|
inlineprotected |
Definition at line 166 of file expr_iterator.h.
|
inline |
Definition at line 79 of file expr_iterator.h.
|
inlineprotected |
Pushes expression onto the stack If overridden, this function should be called from the inheriting class by the override function.
Definition at line 204 of file expr_iterator.h.
|
friend |
Definition at line 76 of file expr_iterator.h.
|
private |
Definition at line 211 of file expr_iterator.h.