|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Public Member Functions | |
| __init__ (self, groups, holders) | |
| statements (self, stmts, before=frozenset()) | |
Public Attributes | |
| groups = groups | |
| holders = set(holders) | |
| int | arms = 0 |
Protected Member Functions | |
| _branch (self, stmts, i, before) | |
| _split (self, stmts, i, site, before) | |
| _renamed (self, stmts, i, before) | |
| _rename (self, arm, stored) | |
Split the module at each dispatched call, copying the rest into one arm per function.
| preprocessor.function_value_dispatch._Dispatch.__init__ | ( | self, | |
| groups, | |||
| holders ) |
|
protected |
Copy the end of `stmts` into each branch of the `if` at `i`, so a call can split.
|
protected |
|
protected |
The names that `stmts[i:]` bind, which each arm renames; refuse when it cannot.
|
protected |
| preprocessor.function_value_dispatch._Dispatch.statements | ( | self, | |
| stmts, | |||
| before = frozenset() ) |
`stmts` with each dispatched call split, and how many copies of the end it holds. `before` holds the names that the enclosing code binds before `stmts`.
| int preprocessor.function_value_dispatch._Dispatch.arms = 0 |
| preprocessor.function_value_dispatch._Dispatch.groups = groups |
| preprocessor.function_value_dispatch._Dispatch.holders = set(holders) |