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

Class SSAToStatDefVisitor

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

All Implemented Interfaces:

com.ibm.wala.ssa.SSAInstruction.IVisitor

public class SSAToStatDefVisitor
extends java.lang.Object
implements com.ibm.wala.ssa.SSAInstruction.IVisitor

Field Summary

Fields

Modifier and Type	Field and Description
boolean	foundStoppingInsn
private com.ibm.wala.ssa.IR	ir
private java.util.HashSet<WalaVarExpr>	noStackSlotVars
private SlotParamTable	slotParamTable
private Stmt	veriStatement

Constructor Summary

Constructors

Constructor and Description
SSAToStatDefVisitor(com.ibm.wala.ssa.IR ir, java.util.HashSet<WalaVarExpr> noStackSlotVars, SlotParamTable slotParamTable)

Method Summary

Modifier and Type	Method and Description
private void	addToNoStackSlotVars(WalaVarExpr wve)
Stmt	convert(com.ibm.wala.ssa.SSAInstruction ssa)
private boolean	extractStackSlotStmt(WalaVarExpr wve)
void	visitArrayLength(com.ibm.wala.ssa.SSAArrayLengthInstruction ssaArrayLengthInstruction)
void	visitArrayLoad(com.ibm.wala.ssa.SSAArrayLoadInstruction ssaArrayLoadInstruction)
void	visitArrayStore(com.ibm.wala.ssa.SSAArrayStoreInstruction ssaArrayStoreInstruction)
void	visitBinaryOp(com.ibm.wala.ssa.SSABinaryOpInstruction ssa)
void	visitCheckCast(com.ibm.wala.ssa.SSACheckCastInstruction ssaCheckCastInstruction)
void	visitComparison(com.ibm.wala.ssa.SSAComparisonInstruction ssa)
void	visitConditionalBranch(com.ibm.wala.ssa.SSAConditionalBranchInstruction ssaConditionalBranchInstruction)
void	visitConversion(com.ibm.wala.ssa.SSAConversionInstruction ssaConversionInstruction)
void	visitGet(com.ibm.wala.ssa.SSAGetInstruction ssaGetInstruction)
void	visitGetCaughtException(com.ibm.wala.ssa.SSAGetCaughtExceptionInstruction ssaGetCaughtExceptionInstruction)
void	visitGoto(com.ibm.wala.ssa.SSAGotoInstruction ssaGotoInstruction)
void	visitInstanceof(com.ibm.wala.ssa.SSAInstanceofInstruction ssaInstanceofInstruction)
void	visitInvoke(com.ibm.wala.ssa.SSAInvokeInstruction ssaInvokeInstruction)
void	visitLoadMetadata(com.ibm.wala.ssa.SSALoadMetadataInstruction ssaLoadMetadataInstruction)
void	visitMonitor(com.ibm.wala.ssa.SSAMonitorInstruction ssaMonitorInstruction)
void	visitNew(com.ibm.wala.ssa.SSANewInstruction ssaNewInstruction)
void	visitPhi(com.ibm.wala.ssa.SSAPhiInstruction ssaPhiInstruction)
void	visitPi(com.ibm.wala.ssa.SSAPiInstruction ssaPiInstruction)
void	visitPut(com.ibm.wala.ssa.SSAPutInstruction ssaPutInstruction)
void	visitReturn(com.ibm.wala.ssa.SSAReturnInstruction ssaReturnInstruction)
void	visitSwitch(com.ibm.wala.ssa.SSASwitchInstruction ssaSwitchInstruction)
void	visitThrow(com.ibm.wala.ssa.SSAThrowInstruction ssaThrowInstruction)
void	visitUnaryOp(com.ibm.wala.ssa.SSAUnaryOpInstruction ssa)

Methods inherited from class java.lang.Object

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

Field Detail

noStackSlotVars

private final java.util.HashSet<WalaVarExpr> noStackSlotVars

slotParamTable

private final SlotParamTable slotParamTable

foundStoppingInsn

public boolean foundStoppingInsn

veriStatement

private Stmt veriStatement

ir

private final com.ibm.wala.ssa.IR ir

Constructor Detail

SSAToStatDefVisitor

public SSAToStatDefVisitor(com.ibm.wala.ssa.IR ir,
                           java.util.HashSet<WalaVarExpr> noStackSlotVars,
                           SlotParamTable slotParamTable)

Method Detail

convert

public Stmt convert(com.ibm.wala.ssa.SSAInstruction ssa)

extractStackSlotStmt

private boolean extractStackSlotStmt(WalaVarExpr wve)

addToNoStackSlotVars

private void addToNoStackSlotVars(WalaVarExpr wve)

visitGoto

public void visitGoto(com.ibm.wala.ssa.SSAGotoInstruction ssaGotoInstruction)

Specified by:

visitGoto in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitArrayLoad

public void visitArrayLoad(com.ibm.wala.ssa.SSAArrayLoadInstruction ssaArrayLoadInstruction)

Specified by:

visitArrayLoad in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitArrayStore

public void visitArrayStore(com.ibm.wala.ssa.SSAArrayStoreInstruction ssaArrayStoreInstruction)

Specified by:

visitArrayStore in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitBinaryOp

public void visitBinaryOp(com.ibm.wala.ssa.SSABinaryOpInstruction ssa)

Specified by:

visitBinaryOp in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitUnaryOp

public void visitUnaryOp(com.ibm.wala.ssa.SSAUnaryOpInstruction ssa)

Specified by:

visitUnaryOp in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitConversion

public void visitConversion(com.ibm.wala.ssa.SSAConversionInstruction ssaConversionInstruction)

Specified by:

visitConversion in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitComparison

public void visitComparison(com.ibm.wala.ssa.SSAComparisonInstruction ssa)

Specified by:

visitComparison in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitConditionalBranch

public void visitConditionalBranch(com.ibm.wala.ssa.SSAConditionalBranchInstruction ssaConditionalBranchInstruction)

Specified by:

visitConditionalBranch in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitSwitch

public void visitSwitch(com.ibm.wala.ssa.SSASwitchInstruction ssaSwitchInstruction)

Specified by:

visitSwitch in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitReturn

public void visitReturn(com.ibm.wala.ssa.SSAReturnInstruction ssaReturnInstruction)

Specified by:

visitReturn in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitGet

public void visitGet(com.ibm.wala.ssa.SSAGetInstruction ssaGetInstruction)

Specified by:

visitGet in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitPut

public void visitPut(com.ibm.wala.ssa.SSAPutInstruction ssaPutInstruction)

Specified by:

visitPut in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitInvoke

public void visitInvoke(com.ibm.wala.ssa.SSAInvokeInstruction ssaInvokeInstruction)

Specified by:

visitInvoke in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitNew

public void visitNew(com.ibm.wala.ssa.SSANewInstruction ssaNewInstruction)

Specified by:

visitNew in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitArrayLength

public void visitArrayLength(com.ibm.wala.ssa.SSAArrayLengthInstruction ssaArrayLengthInstruction)

Specified by:

visitArrayLength in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitThrow

public void visitThrow(com.ibm.wala.ssa.SSAThrowInstruction ssaThrowInstruction)

Specified by:

visitThrow in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitMonitor

public void visitMonitor(com.ibm.wala.ssa.SSAMonitorInstruction ssaMonitorInstruction)

Specified by:

visitMonitor in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitCheckCast

public void visitCheckCast(com.ibm.wala.ssa.SSACheckCastInstruction ssaCheckCastInstruction)

Specified by:

visitCheckCast in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitInstanceof

public void visitInstanceof(com.ibm.wala.ssa.SSAInstanceofInstruction ssaInstanceofInstruction)

Specified by:

visitInstanceof in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitPhi

public void visitPhi(com.ibm.wala.ssa.SSAPhiInstruction ssaPhiInstruction)

Specified by:

visitPhi in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitPi

public void visitPi(com.ibm.wala.ssa.SSAPiInstruction ssaPiInstruction)

Specified by:

visitPi in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitGetCaughtException

public void visitGetCaughtException(com.ibm.wala.ssa.SSAGetCaughtExceptionInstruction ssaGetCaughtExceptionInstruction)

Specified by:

visitGetCaughtException in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitLoadMetadata

public void visitLoadMetadata(com.ibm.wala.ssa.SSALoadMetadataInstruction ssaLoadMetadataInstruction)

Specified by:

visitLoadMetadata in interface com.ibm.wala.ssa.SSAInstruction.IVisitor