Home Original page

CBMC: depth_iterator_baset< depth_iterator_t > Class Template Reference

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.
 
depth_iterator_t & next_sibling_or_parent ()
 
depth_iterator_t operator++ (int)
 Post-increment operator Expensive copy.
 
const exprt & operator* () const
 Dereference operator Dereferencing end() iterator is undefined behaviour.
 
const exprt * operator-> () const
 Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.
 

Protected Member Functions

 depth_iterator_baset ()=default
 Create end iterator.
 
 depth_iterator_baset (const exprt &root)
 Create begin iterator, starting at the supplied node.
 
 ~depth_iterator_baset ()=default
 Destructor Protected to discourage upcasting.
 
 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.
 
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.
 

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 68 of file expr_iterator.h.

◆ difference_type

◆ iterator_category

◆ pointer

◆ value_type

◆ depth_iterator_baset() [1/4]

◆ depth_iterator_baset() [2/4]

Create begin iterator, starting at the supplied node.

Definition at line 157 of file expr_iterator.h.

◆ ~depth_iterator_baset()

Destructor Protected to discourage upcasting.

◆ depth_iterator_baset() [3/4]

◆ depth_iterator_baset() [4/4]

◆ downcast()

◆ get_root()

◆ mutate()

Obtain non-const exprt reference.

Performs a copy-on-write on the root node as a side effect.

Definition at line 184 of file expr_iterator.h.

◆ next_sibling_or_parent()

◆ operator!=()

◆ operator*()

Dereference operator Dereferencing end() iterator is undefined behaviour.

Definition at line 141 of file expr_iterator.h.

◆ operator++() [1/2]

Preincrement operator Do not call on the end() iterator.

Definition at line 96 of file expr_iterator.h.

◆ operator++() [2/2]

Post-increment operator Expensive copy.

Avoid if possible

Definition at line 132 of file expr_iterator.h.

◆ operator->()

Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.

Definition at line 149 of file expr_iterator.h.

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator==()

◆ push_expr()

Pushes expression onto the stack If overridden, this function should be called from the inheriting class by the override function.

Returns
true if element was successfully pushed onto the stack, false otherwise. If returning false, child will not be iterated over.

Definition at line 206 of file expr_iterator.h.

◆ depth_iterator_baset

◆ m_stack

The documentation for this class was generated from the following file: