ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
preprocessor.unbound_locals._Analysis Class Reference

Public Member Functions

 __init__ (self, candidates)
 flow (self, stmts, bound)

Public Attributes

 candidates = candidates
dict unsafe_reads = {}

Protected Member Functions

 _effect (self, stmt, bound)

Detailed Description

Definite assignment over one function body; bindings never unbind.

Constructor & Destructor Documentation

◆ __init__()

preprocessor.unbound_locals._Analysis.__init__ ( self,
candidates )

Member Function Documentation

◆ _effect()

preprocessor.unbound_locals._Analysis._effect ( self,
stmt,
bound )
protected

◆ flow()

preprocessor.unbound_locals._Analysis.flow ( self,
stmts,
bound )
Return the names bound after `stmts`, or None if the end is unreachable.

Member Data Documentation

◆ candidates

preprocessor.unbound_locals._Analysis.candidates = candidates

◆ unsafe_reads

dict preprocessor.unbound_locals._Analysis.unsafe_reads = {}

The documentation for this class was generated from the following file: