|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Public Member Functions | |
| __init__ (self, flagged, unsafe_reads, error) | |
| rewrite (self, stmts) | |
Public Attributes | |
| flagged = flagged | |
| unsafe_reads = unsafe_reads | |
| error = error | |
Protected Member Functions | |
| _rewrite_children (self, stmt) | |
Insert the flag updates and guards for the names in `flagged`.
| preprocessor.unbound_locals._Rewriter.__init__ | ( | self, | |
| flagged, | |||
| unsafe_reads, | |||
| error ) |
|
protected |
| preprocessor.unbound_locals._Rewriter.rewrite | ( | self, | |
| stmts ) |
Return `stmts` with the guards before and the flag updates after.
| preprocessor.unbound_locals._Rewriter.error = error |
| preprocessor.unbound_locals._Rewriter.flagged = flagged |
| preprocessor.unbound_locals._Rewriter.unsafe_reads = unsafe_reads |