Package gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases

Class Summary

Class	Description
SPFCaseList
SpfCasesPass1Visitor
SpfCasesPass2Visitor	This is the second pass of the SPFCases where the SPFCases nodes are eliminated and instead the dynamic region is populated with the predicates for the SPFCases.
SpfToGreenExprVisitor
SpfToGreenVisitor	Main visitor that visits all statements and translate them to the appropriate green expression.

Enum Summary

Enum	Description
SpfCasesInstruction	This is the first pass of SPFCases that creates SPFCases nodes.