|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
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) |
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__()`.
|
protected |
|
protected |
Top-level classes defining both __iter__ and __next__.
|
protected |
|
protected |
The nodes of `scope`'s own body, not of the scopes nested in it.
|
protected |
`(name, value)` for a statement `name = value`, else `(None, None)`.
|
protected |
The `next(name)` calls among `nodes`, and every read of `name`.
| preprocessor.iter_next_lowering.lower_iter_next | ( | module | ) |
Lowers iter()/next() pairs throughout `module` (#8284).
|
protected |