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

Class Summary

Class	Description
LocalOutputInvariantVisitor
ValidGreenPredicate	This class is used to check the invariant that after AstToGreen translation, that the result is a valid Green expression that does not have IfThenElseExpr, WalaVarExpr, FieldRefVarExpr or GammaVarExpr.