CBMC
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
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>

+ Inheritance diagram for depth_iterator_baset< depth_iterator_t >:
[フレーム]
[legend]
+ Collaboration diagram for depth_iterator_baset< depth_iterator_t >:
[フレーム]
[legend]

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.
 

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

Member Typedef Documentation

◆  difference_type

typedef void depth_iterator_baset< depth_iterator_t >::difference_type

Definition at line 71 of file expr_iterator.h.

◆  iterator_category

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

Definition at line 75 of file expr_iterator.h.

◆  pointer

typedef const exprt* depth_iterator_baset< depth_iterator_t >::pointer

Definition at line 73 of file expr_iterator.h.

◆  reference

typedef const exprt& depth_iterator_baset< depth_iterator_t >::reference

Definition at line 74 of file expr_iterator.h.

◆  value_type

typedef exprt depth_iterator_baset< depth_iterator_t >::value_type

Definition at line 72 of file expr_iterator.h.

Constructor & Destructor Documentation

◆  depth_iterator_baset() [1/4]

depth_iterator_baset< depth_iterator_t >::depth_iterator_baset ( )
protecteddefault

Create end iterator.

◆  depth_iterator_baset() [2/4]

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

Create begin iterator, starting at the supplied node.

Definition at line 157 of file expr_iterator.h.

◆  ~depth_iterator_baset()

depth_iterator_baset< depth_iterator_t >::~depth_iterator_baset ( )
protecteddefault

Destructor Protected to discourage upcasting.

◆  depth_iterator_baset() [3/4]

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

◆  depth_iterator_baset() [4/4]

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

Definition at line 165 of file expr_iterator.h.

Member Function Documentation

◆  downcast()

depth_iterator_t & depth_iterator_baset< depth_iterator_t >::downcast ( )
inlineprivate

Definition at line 215 of file expr_iterator.h.

◆  get_root()

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

Definition at line 174 of file expr_iterator.h.

◆  mutate()

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

◆  next_sibling_or_parent()

depth_iterator_t & depth_iterator_baset< depth_iterator_t >::next_sibling_or_parent ( )
inline

Definition at line 118 of file expr_iterator.h.

◆  operator!=()

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

Definition at line 88 of file expr_iterator.h.

◆  operator*()

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

Dereference operator Dereferencing end() iterator is undefined behaviour.

Definition at line 141 of file expr_iterator.h.

◆  operator++() [1/2]

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

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

Definition at line 96 of file expr_iterator.h.

◆  operator++() [2/2]

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

Post-increment operator Expensive copy.

Avoid if possible

Definition at line 132 of file expr_iterator.h.

◆  operator->()

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

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

Definition at line 149 of file expr_iterator.h.

◆  operator=() [1/2]

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

◆  operator=() [2/2]

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

Definition at line 168 of file expr_iterator.h.

◆  operator==()

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

Definition at line 81 of file expr_iterator.h.

◆  push_expr()

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

Friends And Related Symbol Documentation

◆  depth_iterator_baset

friend class depth_iterator_baset
friend

Definition at line 78 of file expr_iterator.h.

Member Data Documentation

◆  m_stack

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

Definition at line 213 of file expr_iterator.h.

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

AltStyle によって変換されたページ (->オリジナル) /