|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Public Member Functions | |
| __init__ (self, candidates) | |
| flow (self, stmts, bound) | |
Public Attributes | |
| candidates = candidates | |
| dict | unsafe_reads = {} |
Protected Member Functions | |
| _effect (self, stmt, bound) | |
Definite assignment over one function body; bindings never unbind.
| preprocessor.unbound_locals._Analysis.__init__ | ( | self, | |
| candidates ) |
|
protected |
| preprocessor.unbound_locals._Analysis.flow | ( | self, | |
| stmts, | |||
| bound ) |
Return the names bound after `stmts`, or None if the end is unreachable.
| preprocessor.unbound_locals._Analysis.candidates = candidates |
| dict preprocessor.unbound_locals._Analysis.unsafe_reads = {} |