|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Functions | |
| _bound_names (module) | |
| _plain_call (node, name, nargs) | |
| _zip_build (stmt) | |
| _loop (stmt, build, counter) | |
| _statement_lists (module) | |
| lower_zip_builds (module) | |
| _zip_binding (stmt) | |
| _is_zip_call (node) | |
| _mentions (tree, name) | |
| _reader (stmt, name) | |
| _inline_zip (stmts, i, module) | |
| inline_zip_names (module) | |
Lower `T = dict(zip(A, B))` to a loop (#8283). `zip` is lowered as a for loop's iterable and inside `list(...)`, but building a dict from it reached the unsupported-function marker. The assignment becomes an empty dict filled by a loop over the same `zip`.
|
protected |
|
protected |
Moves the zip bound by `stmts[i]` into the one sibling reading it.
|
protected |
|
protected |
|
protected |
|
protected |
Whether `node` is `name(...)` with `nargs` positional arguments.
|
protected |
The `for` loop or `list(name)` call in `stmt` that reads `name`, else None.
|
protected |
|
protected |
`(name, zip_call)` for `name = zip(...)` over names and literals, else None.
|
protected |
`(target, zip_call)` for `target = dict(zip(a, b))`, else None.
| preprocessor.zip_lowering.inline_zip_names | ( | module | ) |
Reads `z = zip(...)` at its one `list(z)` or `for ... in z` (#8967). The iterator is consumed once, so the call moves to its reader, where the existing `list(zip(...))` and `for ... in zip(...)` lowerings apply. Its operands are names and literals not rebound in between, so they evaluate to the same objects.
| preprocessor.zip_lowering.lower_zip_builds | ( | module | ) |
Rewrites every eligible zip-built dict in `module`.