|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Functions | |
| _bound_names (node) | |
| _imports (module) | |
| _itertools_names (module, counts) | |
| _function (func, names) | |
| _repeat_operands (call) | |
| _as_list (call, names) | |
| _drained (node, counts) | |
| _drain_once (stmt, name, counts) | |
| _is_stable (node, rebindable) | |
| _inline_single_use (block, names, counts, loads, rebindable) | |
| _blocks (module) | |
| lower_itertools (module) | |
Variables | |
| tuple | _FUNCTIONS = ("chain", "repeat") |
| tuple | _DRAINS = ("list", "tuple", "sorted", "set", "sum", "min", "max") |
| tuple | _SIMPLE_STATEMENTS = (ast.Assign, ast.AnnAssign, ast.AugAssign, ast.Expr, ast.Assert, ast.Return) |
| tuple | _LOOPING_SCOPES |
Lower itertools.chain, and itertools.repeat with a count, where a builtin drains the iterator at once (#8377). `list(chain(a, b))` becomes `list(list(a) + list(b))` and `sum(repeat(x, n))` becomes `sum([x] * n)`. A drain runs no code of the program between steps, so the lazy iterator and the list yield the same elements. A name bound to such a call and read once, by a drain in the next statement, is replaced there by the call. Any other use is left as written, which the converter refuses.
|
protected |
The list expression yielding what `call` iterates, or None.
|
protected |
|
protected |
|
protected |
The drain call reading `name` in simple statement `stmt`, run once.
|
protected |
The argument a builtin drain call `node` iterates, or None.
|
protected |
|
protected |
(bound name, function or None for the module) per top-level import from itertools.
|
protected |
|
protected |
Whether `node` reads the same value later in the next statement.
|
protected |
The names bound once, by a top-level import, to the itertools module and to its modelled functions.
|
protected |
| preprocessor.itertools_lowering.lower_itertools | ( | module | ) |
Lower the drained itertools iterators of `module` to lists.
|
protected |
|
protected |
|
protected |
|
protected |