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

Class FieldArrayVarToSPFVarVisitor

java.lang.Object

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

gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor

All Implemented Interfaces:

ExprVisitor<za.ac.sun.cs.green.expr.Expression>

public class FieldArrayVarToSPFVarVisitor
extends ExprMapVisitor
implements ExprVisitor<za.ac.sun.cs.green.expr.Expression>

A visitor that visits all FieldRefVarExpr and generates the appropriate SPF symbolic variable based on its type.

Field Summary

Fields

Modifier and Type	Field and Description
protected ExprVisitorAdapter<za.ac.sun.cs.green.expr.Expression>	eva
private FieldRefTypeTable	fieldRefTypeTable

Constructor Summary

Constructors

Constructor and Description
FieldArrayVarToSPFVarVisitor(FieldRefTypeTable fieldRefTypeTable)

Method Summary

Modifier and Type	Method and Description
za.ac.sun.cs.green.expr.Expression	visit(ArrayRefVarExpr expr)
za.ac.sun.cs.green.expr.Expression	visit(FieldRefVarExpr expr)
za.ac.sun.cs.green.expr.Expression	visit(GammaVarExpr expr)
za.ac.sun.cs.green.expr.Expression	visit(IfThenElseExpr expr)
za.ac.sun.cs.green.expr.Expression	visit(WalaVarExpr expr)

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

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

Methods inherited from interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

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

Field Detail

fieldRefTypeTable

private final FieldRefTypeTable fieldRefTypeTable

eva

protected final ExprVisitorAdapter<za.ac.sun.cs.green.expr.Expression> eva

Constructor Detail

FieldArrayVarToSPFVarVisitor

public FieldArrayVarToSPFVarVisitor(FieldRefTypeTable fieldRefTypeTable)

Method Detail

visit

public za.ac.sun.cs.green.expr.Expression visit(IfThenElseExpr expr)

Specified by:

visit in interface ExprVisitor<za.ac.sun.cs.green.expr.Expression>

Overrides:

visit in class ExprMapVisitor

visit

public za.ac.sun.cs.green.expr.Expression visit(FieldRefVarExpr expr)

Specified by:

visit in interface ExprVisitor<za.ac.sun.cs.green.expr.Expression>

Overrides:

visit in class ExprMapVisitor

visit

public za.ac.sun.cs.green.expr.Expression visit(ArrayRefVarExpr expr)

Specified by:

visit in interface ExprVisitor<za.ac.sun.cs.green.expr.Expression>

Overrides:

visit in class ExprMapVisitor

visit

public za.ac.sun.cs.green.expr.Expression visit(WalaVarExpr expr)

Specified by:

visit in interface ExprVisitor<za.ac.sun.cs.green.expr.Expression>

Overrides:

visit in class ExprMapVisitor

visit

public za.ac.sun.cs.green.expr.Expression visit(GammaVarExpr expr)

Specified by:

visit in interface ExprVisitor<za.ac.sun.cs.green.expr.Expression>

Overrides:

visit in class ExprMapVisitor