|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Public Member Functions | |
| __init__ (self, gen_defs, whole_value, new_scope, branching) | |
| visit (self, n, scope, ctx) | |
Public Attributes | |
| gen_defs = gen_defs | |
| whole_value = whole_value | |
| new_scope = new_scope | |
| branching = branching | |
| list | scopes = [{"all": set(), "stored": set(), "function": False}] |
| func_scope | |
| bindings | |
| calls | |
| dict | stores = {}, {}, {}, {} |
Protected Member Functions | |
| _record (self, n, scope, ctx) | |
| _is_generator_binding (self, n) | |
| _visit_scope (self, n) | |
| _child_ctx (self, n, field, ctx) | |
Static Protected Member Functions | |
| _params (fn) | |
Per scope, the names used and stored, each `g = genfunc(...)` binding and each `next(g)` call, with the context it runs in: "linear", "loop", "try" or "branch".
| preprocessor.generator_mixin._GeneratorConsumerScan.__init__ | ( | self, | |
| gen_defs, | |||
| whole_value, | |||
| new_scope, | |||
| branching ) |
|
protected |
|
protected |
|
staticprotected |
|
protected |
|
protected |
| preprocessor.generator_mixin._GeneratorConsumerScan.visit | ( | self, | |
| n, | |||
| scope, | |||
| ctx ) |
| preprocessor.generator_mixin._GeneratorConsumerScan.bindings |
| preprocessor.generator_mixin._GeneratorConsumerScan.branching = branching |
| preprocessor.generator_mixin._GeneratorConsumerScan.calls |
| preprocessor.generator_mixin._GeneratorConsumerScan.func_scope |
| preprocessor.generator_mixin._GeneratorConsumerScan.gen_defs = gen_defs |
| preprocessor.generator_mixin._GeneratorConsumerScan.new_scope = new_scope |
| list preprocessor.generator_mixin._GeneratorConsumerScan.scopes = [{"all": set(), "stored": set(), "function": False}] |
| dict preprocessor.generator_mixin._GeneratorConsumerScan.stores = {}, {}, {}, {} |
| preprocessor.generator_mixin._GeneratorConsumerScan.whole_value = whole_value |