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

Class AstToGreenVisitor

java.lang.Object

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

All Implemented Interfaces:

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

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

Main visitor that visits all statements and translate them to the appropriate green expression. At the point the expected statements are, assignments, composition and skip.

Field Summary

Fields

Modifier and Type	Field and Description
(package private) ExprVisitorAdapter<za.ac.sun.cs.green.expr.Expression>	eva
(package private) AstToGreenExprVisitor	exprVisitor
java.util.ArrayList<za.ac.sun.cs.green.expr.Expression>	greenList
java.util.ArrayList<Stmt>	stmtList

Constructor Summary

Constructors

Constructor and Description
AstToGreenVisitor()

Method Summary

Modifier and Type	Method and Description
za.ac.sun.cs.green.expr.Expression	assignStmt(AssignmentStmt stmt)
za.ac.sun.cs.green.expr.Expression	bad(java.lang.Object obj)
za.ac.sun.cs.green.expr.Expression	compositionStmt(CompositionStmt stmt) Transform a composition statement into a conjunction in green.
static DynamicRegion	execute(DynamicRegion dynRegion)
za.ac.sun.cs.green.expr.Expression	transform(Stmt stmt)
za.ac.sun.cs.green.expr.Expression	visit(ArrayLengthInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(ArrayLoadInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(ArrayStoreInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(AssignmentStmt a)
za.ac.sun.cs.green.expr.Expression	visit(CheckCastInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(CompositionStmt a)
za.ac.sun.cs.green.expr.Expression	visit(GetInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(IfThenElseStmt a)
za.ac.sun.cs.green.expr.Expression	visit(InstanceOfInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(InvokeInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(NewInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(PhiInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(PutInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(ReturnInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(SkipStmt a)
za.ac.sun.cs.green.expr.Expression	visit(SPFCaseStmt c)
za.ac.sun.cs.green.expr.Expression	visit(SwitchInstruction c)
za.ac.sun.cs.green.expr.Expression	visit(ThrowInstruction c)

Methods inherited from class java.lang.Object

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

Field Detail

greenList

public final java.util.ArrayList<za.ac.sun.cs.green.expr.Expression> greenList

stmtList

public final java.util.ArrayList<Stmt> stmtList

eva

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

exprVisitor

AstToGreenExprVisitor exprVisitor

Constructor Detail

AstToGreenVisitor

public AstToGreenVisitor()

Method Detail

bad

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

assignStmt

public za.ac.sun.cs.green.expr.Expression assignStmt(AssignmentStmt stmt)

compositionStmt

public za.ac.sun.cs.green.expr.Expression compositionStmt(CompositionStmt stmt)

Transform a composition statement into a conjunction in green.

Parameters:

stmt - The composition statement to be translated.

Returns:

A green expression that represents the compsition statement.

transform

public za.ac.sun.cs.green.expr.Expression transform(Stmt stmt)

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

visit

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

Specified by:

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

execute

public static DynamicRegion execute(DynamicRegion dynRegion)
                             throws za.ac.sun.cs.green.expr.VisitorException

Throws:

za.ac.sun.cs.green.expr.VisitorException