Depth first search iterator base - iterates over supplied expression and all its operands recursively. More...

#include <expr_iterator.h>

Inheritance diagram for depth_iterator_baset< depth_iterator_t >:

Collaboration diagram for depth_iterator_baset< depth_iterator_t >:

Public Types
typedef void	difference_type

typedef exprt	value_type

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...

Public Attributes
const typedef exprt *	pointer

const typedef exprt &	reference

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

Detailed Description

template<typename depth_iterator_t>
class depth_iterator_baset< depth_iterator_t >

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.

Member Typedef Documentation

◆ difference_type

template<typename depth_iterator_t >

typedef void depth_iterator_baset< depth_iterator_t >::difference_type

Definition at line 69 of file expr_iterator.h.

◆ iterator_category

template<typename depth_iterator_t >

typedef std::forward_iterator_tag depth_iterator_baset< depth_iterator_t >::iterator_category

Definition at line 73 of file expr_iterator.h.

◆ value_type

template<typename depth_iterator_t >

typedef exprt depth_iterator_baset< depth_iterator_t >::value_type

Definition at line 70 of file expr_iterator.h.

Constructor & Destructor Documentation

◆ depth_iterator_baset() [1/4]

template<typename depth_iterator_t >

depth_iterator_baset< depth_iterator_t >::depth_iterator_baset ( )

protecteddefault

Create end iterator.

◆ depth_iterator_baset() [2/4]

template<typename depth_iterator_t >

depth_iterator_baset< depth_iterator_t >::depth_iterator_baset ( const exprt & root )

inlineexplicitprotected

Create begin iterator, starting at the supplied node.

Definition at line 155 of file expr_iterator.h.

◆ ~depth_iterator_baset()

template<typename depth_iterator_t >

depth_iterator_baset< depth_iterator_t >::~depth_iterator_baset ( )

protecteddefault

Destructor Protected to discourage upcasting.

◆ depth_iterator_baset() [3/4]

template<typename depth_iterator_t >

depth_iterator_baset< depth_iterator_t >::depth_iterator_baset ( const depth_iterator_baset< depth_iterator_t > & )

protecteddefault

◆ depth_iterator_baset() [4/4]

template<typename depth_iterator_t >

depth_iterator_baset< depth_iterator_t >::depth_iterator_baset ( depth_iterator_baset< depth_iterator_t > && other )

inlineprotected

Definition at line 163 of file expr_iterator.h.

Member Function Documentation

◆ downcast()

template<typename depth_iterator_t >

depth_iterator_t& depth_iterator_baset< depth_iterator_t >::downcast ( )

inlineprivate

Definition at line 213 of file expr_iterator.h.

◆ get_root()

template<typename depth_iterator_t >

const exprt& depth_iterator_baset< depth_iterator_t >::get_root ( )

inlineprotected

Definition at line 172 of file expr_iterator.h.

◆ mutate()

template<typename depth_iterator_t >

exprt& depth_iterator_baset< depth_iterator_t >::mutate ( )

inlineprotected

Obtain non-const exprt reference.

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

Remarks: To be called only if a the root is a non-const exprt. Do not call on the end() iterator

Definition at line 182 of file expr_iterator.h.

◆ next_sibling_or_parent()

template<typename depth_iterator_t >

depth_iterator_t& depth_iterator_baset< depth_iterator_t >::next_sibling_or_parent ( )

inline

Definition at line 116 of file expr_iterator.h.

◆ operator!=()

template<typename depth_iterator_t >

template<typename other_depth_iterator_t >

bool depth_iterator_baset< depth_iterator_t >::operator!= ( const depth_iterator_baset< other_depth_iterator_t > & other ) const

inline

Definition at line 86 of file expr_iterator.h.

◆ operator*()

template<typename depth_iterator_t >

const exprt& depth_iterator_baset< depth_iterator_t >::operator* ( ) const

inline

Dereference operator Dereferencing end() iterator is undefined behaviour.

Definition at line 139 of file expr_iterator.h.

◆ operator++() [1/2]

template<typename depth_iterator_t >

depth_iterator_t& depth_iterator_baset< depth_iterator_t >::operator++ ( )

inline

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

Definition at line 94 of file expr_iterator.h.

◆ operator++() [2/2]

template<typename depth_iterator_t >

depth_iterator_t depth_iterator_baset< depth_iterator_t >::operator++ ( int )

inline

Post-increment operator Expensive copy.

Avoid if possible

Definition at line 130 of file expr_iterator.h.

◆ operator->()

template<typename depth_iterator_t >

const exprt* depth_iterator_baset< depth_iterator_t >::operator-> ( ) const

inline

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

Definition at line 147 of file expr_iterator.h.

◆ operator=() [1/2]

template<typename depth_iterator_t >

depth_iterator_baset& depth_iterator_baset< depth_iterator_t >::operator= ( const depth_iterator_baset< depth_iterator_t > & )

protecteddefault

◆ operator=() [2/2]

template<typename depth_iterator_t >

depth_iterator_baset& depth_iterator_baset< depth_iterator_t >::operator= ( depth_iterator_baset< depth_iterator_t > && other )

inlineprotected

Definition at line 166 of file expr_iterator.h.

◆ operator==()

template<typename depth_iterator_t >

template<typename other_depth_iterator_t >

bool depth_iterator_baset< depth_iterator_t >::operator== ( const depth_iterator_baset< other_depth_iterator_t > & other ) const

inline

Definition at line 79 of file expr_iterator.h.

◆ push_expr()

template<typename depth_iterator_t >

bool depth_iterator_baset< depth_iterator_t >::push_expr ( const exprt & expr )

inlineprotected

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

Friends And Related Function Documentation

◆ depth_iterator_baset

template<typename depth_iterator_t >

template<typename other_depth_iterator_t >

friend class depth_iterator_baset

friend

Definition at line 76 of file expr_iterator.h.

Member Data Documentation

◆ m_stack

template<typename depth_iterator_t >

std::deque<depth_iterator_expr_statet> depth_iterator_baset< depth_iterator_t >::m_stack

private

Definition at line 211 of file expr_iterator.h.

◆ pointer

template<typename depth_iterator_t >

const typedef exprt* depth_iterator_baset< depth_iterator_t >::pointer

Definition at line 71 of file expr_iterator.h.

◆ reference

template<typename depth_iterator_t >

const typedef exprt& depth_iterator_baset< depth_iterator_t >::reference

Definition at line 72 of file expr_iterator.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/util/expr_iterator.h

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Private Member Functions

Private Attributes

Friends

Detailed Description

template<typename depth_iterator_t> class depth_iterator_baset< depth_iterator_t >

Member Typedef Documentation

◆ difference_type

◆ iterator_category

◆ value_type

Constructor & Destructor Documentation

◆ depth_iterator_baset() [1/4]

◆ depth_iterator_baset() [2/4]

◆ ~depth_iterator_baset()

◆ depth_iterator_baset() [3/4]

◆ depth_iterator_baset() [4/4]

Member Function Documentation

◆ downcast()

◆ get_root()

◆ mutate()

◆ next_sibling_or_parent()

◆ operator!=()

◆ operator*()

◆ operator++() [1/2]

◆ operator++() [2/2]

◆ operator->()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator==()

◆ push_expr()

Friends And Related Function Documentation

◆ depth_iterator_baset

Member Data Documentation

◆ m_stack

◆ pointer

◆ reference

template<typename depth_iterator_t>
class depth_iterator_baset< depth_iterator_t >