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

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)

Detailed Description

Insert the flag updates and guards for the names in `flagged`.

Constructor & Destructor Documentation

◆ __init__()

preprocessor.unbound_locals._Rewriter.__init__ ( self,
flagged,
unsafe_reads,
error )

Member Function Documentation

◆ _rewrite_children()

preprocessor.unbound_locals._Rewriter._rewrite_children ( self,
stmt )
protected

◆ rewrite()

preprocessor.unbound_locals._Rewriter.rewrite ( self,
stmts )
Return `stmts` with the guards before and the flag updates after.

Member Data Documentation

◆ error

preprocessor.unbound_locals._Rewriter.error = error

◆ flagged

preprocessor.unbound_locals._Rewriter.flagged = flagged

◆ unsafe_reads

preprocessor.unbound_locals._Rewriter.unsafe_reads = unsafe_reads

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