|
CBMC
|
#include <expr_iterator.h>
Inheritance diagram for const_unique_depth_iteratort:
Collaboration diagram for const_unique_depth_iteratort:Public Member Functions | |
| const_unique_depth_iteratort (const exprt &expr) | |
| Create iterator starting at the supplied node (root) More... | |
| const_unique_depth_iteratort ()=default | |
| Create an end iterator. More... | |
Public Member Functions inherited from depth_iterator_baset< const_unique_depth_iteratort > | |
| bool | operator== (const depth_iterator_baset< other_depth_iterator_t > &other) const |
| bool | operator!= (const depth_iterator_baset< other_depth_iterator_t > &other) const |
| const_unique_depth_iteratort & | operator++ () |
| Preincrement operator Do not call on the end() iterator. More... | |
| const_unique_depth_iteratort | operator++ (int) |
| Post-increment operator Expensive copy. More... | |
| const_unique_depth_iteratort & | next_sibling_or_parent () |
| 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... | |
Private Member Functions | |
| bool | push_expr (const exprt &expr) |
| Push expression onto the stack and add to the set of traversed exprts. More... | |
Private Attributes | |
| friend | depth_iterator_baset |
| std::set< exprt > | m_traversed |
Additional Inherited Members | |
Public Types inherited from depth_iterator_baset< const_unique_depth_iteratort > | |
| typedef void | difference_type |
| typedef exprt | value_type |
| typedef std::forward_iterator_tag | iterator_category |
Public Attributes inherited from depth_iterator_baset< const_unique_depth_iteratort > | |
| const typedef exprt * | pointer |
| const typedef exprt & | reference |
Protected Member Functions inherited from depth_iterator_baset< const_unique_depth_iteratort > | |
| 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 (const depth_iterator_baset &)=default | |
| depth_iterator_baset (depth_iterator_baset &&other) | |
| ~depth_iterator_baset ()=default | |
| Destructor Protected to discourage upcasting. More... | |
| 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... | |
Definition at line 285 of file expr_iterator.h.
|
inlineexplicit |
Create iterator starting at the supplied node (root)
Definition at line 291 of file expr_iterator.h.
|
default |
Create an end iterator.
|
inlineprivate |
Push expression onto the stack and add to the set of traversed exprts.
Definition at line 298 of file expr_iterator.h.
|
private |
Definition at line 288 of file expr_iterator.h.
|
private |
Definition at line 305 of file expr_iterator.h.