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

Class ValidGreenPredicate

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor<java.lang.Boolean>

gov.nasa.jpf.symbc.veritesting.ast.visitors.ForallExprVisitor

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

All Implemented Interfaces:

ExprVisitor<java.lang.Boolean>

public class ValidGreenPredicate
extends ForallExprVisitor

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.

Field Summary

Fields

Modifier and Type	Field and Description
(package private) java.util.Map<java.lang.Class,java.lang.Integer>	failures

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

combine, defaultVal, eva

Constructor Summary

Constructors

Constructor and Description
ValidGreenPredicate()

Method Summary

Modifier and Type	Method and Description
void	checkInvariant(za.ac.sun.cs.green.expr.Expression expr, java.util.Map<java.lang.Class,java.lang.Integer> failureMap)
(package private) java.lang.Boolean	incrementFailure(za.ac.sun.cs.green.expr.Expression expr)
java.lang.Boolean	visit(FieldRefVarExpr expr)
java.lang.Boolean	visit(GammaVarExpr expr)
java.lang.Boolean	visit(IfThenElseExpr expr)
java.lang.Boolean	visit(WalaVarExpr expr)

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

failures

java.util.Map<java.lang.Class,java.lang.Integer> failures

Constructor Detail

ValidGreenPredicate

public ValidGreenPredicate()

Method Detail

checkInvariant

public void checkInvariant(za.ac.sun.cs.green.expr.Expression expr,
                           java.util.Map<java.lang.Class,java.lang.Integer> failureMap)
                    throws StaticRegionException

Throws:

StaticRegionException

incrementFailure

java.lang.Boolean incrementFailure(za.ac.sun.cs.green.expr.Expression expr)

visit

public java.lang.Boolean visit(IfThenElseExpr expr)

Specified by:

visit in interface ExprVisitor<java.lang.Boolean>

Overrides:

visit in class ExprIterVisitor<java.lang.Boolean>

visit

public java.lang.Boolean visit(WalaVarExpr expr)

Specified by:

visit in interface ExprVisitor<java.lang.Boolean>

Overrides:

visit in class ExprIterVisitor<java.lang.Boolean>

visit

public java.lang.Boolean visit(FieldRefVarExpr expr)

Specified by:

visit in interface ExprVisitor<java.lang.Boolean>

Overrides:

visit in class ExprIterVisitor<java.lang.Boolean>

visit

public java.lang.Boolean visit(GammaVarExpr expr)

Specified by:

visit in interface ExprVisitor<java.lang.Boolean>

Overrides:

visit in class ExprIterVisitor<java.lang.Boolean>