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

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)

Detailed Description

Split the module at each dispatched call, copying the rest into one arm per function.

Constructor & Destructor Documentation

◆ __init__()

preprocessor.function_value_dispatch._Dispatch.__init__ ( self,
groups,
holders )

Member Function Documentation

◆ _branch()

preprocessor.function_value_dispatch._Dispatch._branch ( self,
stmts,
i,
before )
protected
Copy the end of `stmts` into each branch of the `if` at `i`, so a call can split.

◆ _rename()

preprocessor.function_value_dispatch._Dispatch._rename ( self,
arm,
stored )
protected

◆ _renamed()

preprocessor.function_value_dispatch._Dispatch._renamed ( self,
stmts,
i,
before )
protected
The names that `stmts[i:]` bind, which each arm renames; refuse when it cannot.

◆ _split()

preprocessor.function_value_dispatch._Dispatch._split ( self,
stmts,
i,
site,
before )
protected

◆ statements()

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`.

Member Data Documentation

◆ arms

int preprocessor.function_value_dispatch._Dispatch.arms = 0

◆ groups

preprocessor.function_value_dispatch._Dispatch.groups = groups

◆ holders

preprocessor.function_value_dispatch._Dispatch.holders = set(holders)

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