ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
preprocessor.iter_next_lowering Namespace Reference

Classes

class  _Lowering

Functions

 _scope_nodes (scope)
 _is_call (node, name, nargs)
 _single_assignment (node)
 _iterator_classes (module)
 _list_iterator_class (name)
 _uses (nodes, name)
 lower_iter_next (module)

Variables

tuple _SCOPES = (ast.FunctionDef, ast.AsyncFunctionDef, ast.Lambda, ast.ClassDef)

Detailed Description

Lower iter() and next() over a list or a user iterator (#8284).

Neither builtin is modelled, so `g = iter(xs)` was refused and `next(g)` was an
unsupported call. Where `g` is bound once and only ever read as `next(g)`, the
iterator becomes an instance of a small per-site class over `list(xs)`, or, for
an instance of a class defining `__iter__` and `__next__`, that instance's own
`__iter__()`; each `next(g)` becomes `g.__next__()`.

Function Documentation

◆ _is_call()

preprocessor.iter_next_lowering._is_call ( node,
name,
nargs )
protected

◆ _iterator_classes()

preprocessor.iter_next_lowering._iterator_classes ( module)
protected
Top-level classes defining both __iter__ and __next__.

◆ _list_iterator_class()

preprocessor.iter_next_lowering._list_iterator_class ( name)
protected

◆ _scope_nodes()

preprocessor.iter_next_lowering._scope_nodes ( scope)
protected
The nodes of `scope`'s own body, not of the scopes nested in it.

◆ _single_assignment()

preprocessor.iter_next_lowering._single_assignment ( node)
protected
`(name, value)` for a statement `name = value`, else `(None, None)`.

◆ _uses()

preprocessor.iter_next_lowering._uses ( nodes,
name )
protected
The `next(name)` calls among `nodes`, and every read of `name`.

◆ lower_iter_next()

preprocessor.iter_next_lowering.lower_iter_next ( module)
Lowers iter()/next() pairs throughout `module` (#8284).

Variable Documentation

◆ _SCOPES

tuple preprocessor.iter_next_lowering._SCOPES = (ast.FunctionDef, ast.AsyncFunctionDef, ast.Lambda, ast.ClassDef)
protected