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

Class ExpUniqueVisitor

java.lang.Object

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

gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.ExpUniqueVisitor

All Implemented Interfaces:

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

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

Unique Expression Visitor that ensures the uniqueness of vars used inside the region.

Field Summary

Fields

Modifier and Type	Field and Description
(package private) StaticRegionException	sre
(package private) int	uniqueNum

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

eva

Constructor Summary

Constructors

Constructor and Description
ExpUniqueVisitor(int uniqueNum)

Method Summary

Modifier and Type	Method and Description
za.ac.sun.cs.green.expr.Expression	visit(ArrayRefVarExpr expr) A visit to all ArrayRefVarExpr to create a new-unique object for the same var number.
za.ac.sun.cs.green.expr.Expression	visit(AstVarExpr expr)
za.ac.sun.cs.green.expr.Expression	visit(FieldRefVarExpr expr) A visit to all FieldRefVarExpr to create a new-unique object for the same var number.
za.ac.sun.cs.green.expr.Expression	visit(WalaVarExpr expr) A visit to all WalaVariables to create a new-unique object for the same var number.

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

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

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

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

Field Detail

uniqueNum

int uniqueNum

sre

StaticRegionException sre

Constructor Detail

ExpUniqueVisitor

public ExpUniqueVisitor(int uniqueNum)

Method Detail

visit

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

A visit to all WalaVariables to create a new-unique object for the same var number.

Specified by:

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

Overrides:

visit in class ExprMapVisitor

Parameters:

expr - WalaVariable that is visited

Returns:

either a new unique wala var object or already an existing unique wala var object.

visit

public za.ac.sun.cs.green.expr.Expression visit(AstVarExpr 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)

A visit to all FieldRefVarExpr to create a new-unique object for the same var number.

Specified by:

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

Overrides:

visit in class ExprMapVisitor

Parameters:

expr - FieldRefVarExpr that is visited

Returns:

either a new unique FieldRefVarExpr or already an existing unique FieldRefVarExpr object.

visit

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

A visit to all ArrayRefVarExpr to create a new-unique object for the same var number.

Specified by:

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

Overrides:

visit in class ExprMapVisitor

Parameters:

expr - ArrayRefVarExpr that is visited

Returns:

either a new unique ArrayRefVarExpr or already an existing unique ArrayRefVarExpr object.