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

Class AstToGreenExprVisitor

java.lang.Object

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

All Implemented Interfaces:

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

public class AstToGreenExprVisitor
extends java.lang.Object
implements ExprVisitor<za.ac.sun.cs.green.expr.Expression>

This is a visitor class that Translate expression in RangerIR to te appropriate Green expression.

Field Summary

Fields

Modifier and Type	Field and Description
(package private) za.ac.sun.cs.green.expr.Expression	currentCondition
DefUseVisit	defUseVisit
(package private) ExprVisitorAdapter<za.ac.sun.cs.green.expr.Expression>	eva
(package private) za.ac.sun.cs.green.expr.Expression	toAssign

Constructor Summary

Constructors

Constructor and Description
AstToGreenExprVisitor()

Method Summary

Modifier and Type	Method and Description
za.ac.sun.cs.green.expr.Expression	assign(za.ac.sun.cs.green.expr.Expression e)
static za.ac.sun.cs.green.expr.Expression	bad(java.lang.Object obj)
za.ac.sun.cs.green.expr.Expression	ite(za.ac.sun.cs.green.expr.Expression cond, za.ac.sun.cs.green.expr.Expression thenExpr, za.ac.sun.cs.green.expr.Expression elseExpr) Translates conditional expression to a corresponding Green expression.
void	setAssign(za.ac.sun.cs.green.expr.Expression toAssign)
za.ac.sun.cs.green.expr.Expression	visit(ArrayRefVarExpr expr)
za.ac.sun.cs.green.expr.Expression	visit(AstVarExpr expr)
za.ac.sun.cs.green.expr.Expression	visit(FieldRefVarExpr expr)
za.ac.sun.cs.green.expr.Expression	visit(GammaVarExpr expr) Translating a GammaExpression into an IfThenElseExpression
za.ac.sun.cs.green.expr.Expression	visit(IfThenElseExpr expr) Translating a TfThenElseExpr into an IfThenElseExpression
za.ac.sun.cs.green.expr.Expression	visit(za.ac.sun.cs.green.expr.IntConstant expr)
za.ac.sun.cs.green.expr.Expression	visit(za.ac.sun.cs.green.expr.IntVariable expr)
za.ac.sun.cs.green.expr.Expression	visit(za.ac.sun.cs.green.expr.Operation expr)
za.ac.sun.cs.green.expr.Expression	visit(za.ac.sun.cs.green.expr.RealConstant expr)
za.ac.sun.cs.green.expr.Expression	visit(za.ac.sun.cs.green.expr.RealVariable expr)
za.ac.sun.cs.green.expr.Expression	visit(za.ac.sun.cs.green.expr.StringConstantGreen expr)
za.ac.sun.cs.green.expr.Expression	visit(za.ac.sun.cs.green.expr.StringVariable expr)
za.ac.sun.cs.green.expr.Expression	visit(WalaVarExpr expr)

Methods inherited from class java.lang.Object

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

Field Detail

toAssign

za.ac.sun.cs.green.expr.Expression toAssign

currentCondition

za.ac.sun.cs.green.expr.Expression currentCondition

eva

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

defUseVisit

public DefUseVisit defUseVisit

Constructor Detail

AstToGreenExprVisitor

public AstToGreenExprVisitor()

Method Detail

setAssign

public void setAssign(za.ac.sun.cs.green.expr.Expression toAssign)

bad

public static za.ac.sun.cs.green.expr.Expression bad(java.lang.Object obj)

assign

public za.ac.sun.cs.green.expr.Expression assign(za.ac.sun.cs.green.expr.Expression e)

ite

public za.ac.sun.cs.green.expr.Expression ite(za.ac.sun.cs.green.expr.Expression cond,
                                              za.ac.sun.cs.green.expr.Expression thenExpr,
                                              za.ac.sun.cs.green.expr.Expression elseExpr)

Translates conditional expression to a corresponding Green expression.

Parameters:

cond - Condition inside the expression.

thenExpr - Expression in the then side.

elseExpr - Expression in the else side.

Returns:

Green expression that represents the the IfThenElseExpression.

visit

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

Translating a GammaExpression into an IfThenElseExpression

Specified by:

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

Parameters:

expr - A Gamma expression to be translated.

Returns:

A IfThenElseExpr that needs to be later translated to a Green Expression.

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>

visit

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

Translating a TfThenElseExpr into an IfThenElseExpression

Specified by:

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

Parameters:

expr - A Gamma expression to be translated.

Returns:

A IfThenElseExpr that needs to be later translated to a Green Expression.

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>

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>

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>

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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