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

Class SpfToGreenVisitor

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

All Implemented Interfaces:

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

public class SpfToGreenVisitor
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

Constructor Summary

Constructors

Constructor and Description
SpfToGreenVisitor()

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.
private za.ac.sun.cs.green.expr.Expression	earlyReturnToGreen(za.ac.sun.cs.green.expr.Expression earlyReturnExp, DynamicRegion dynRegion)
DynamicRegion	execute(DynamicRegion dynRegion)
private static SPFCaseStmt	noVars(SPFCaseStmt spfCaseStmt, DynamicRegion dynRegion)
private static za.ac.sun.cs.green.expr.Expression	toGreenSinglePredicate(SPFCaseList greenSPFCaseList)
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

eva

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

exprVisitor

AstToGreenExprVisitor exprVisitor

Constructor Detail

SpfToGreenVisitor

public SpfToGreenVisitor()

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 DynamicRegion execute(DynamicRegion dynRegion)

earlyReturnToGreen

private za.ac.sun.cs.green.expr.Expression earlyReturnToGreen(za.ac.sun.cs.green.expr.Expression earlyReturnExp,
                                                              DynamicRegion dynRegion)

toGreenSinglePredicate

private static za.ac.sun.cs.green.expr.Expression toGreenSinglePredicate(SPFCaseList greenSPFCaseList)

noVars

private static SPFCaseStmt noVars(SPFCaseStmt spfCaseStmt,
                                  DynamicRegion dynRegion)