gov.nasa.jpf.symbc.veritesting.VeritestingUtil

Class SymbCondVisitor

java.lang.Object

gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

All Implemented Interfaces:

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

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

Visits expression in a conditional statement to check if any of its arguments are indeed symbolic.

Field Summary

Fields

Modifier and Type	Field and Description
ExprVisitorAdapter<za.ac.sun.cs.green.expr.Expression>	eva
private boolean	findStackSlotsOnly
private boolean	foundWalaVarExpr
private boolean	isSymCondition
java.util.HashSet<WalaVarExpr>	noStackSlotVars
private gov.nasa.jpf.vm.StackFrame	sf
private SlotParamTable	slotParamTable
boolean	stackSlotNotFound
private com.ibm.wala.ssa.SymbolTable	symbolTable

Constructor Summary

Constructors

Constructor and Description
SymbCondVisitor(gov.nasa.jpf.vm.StackFrame sf, SlotParamTable slotParamTable, boolean findStackSlotsOnly, com.ibm.wala.ssa.SymbolTable symbolTable)

Method Summary

Modifier and Type	Method and Description
static java.util.HashSet<WalaVarExpr>	execute(com.ibm.wala.ssa.IR ir, SlotParamTable slotParamTable, Stmt staticStmt)
boolean	isFoundWalaVarExpr()
boolean	isSymCondition()
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)
za.ac.sun.cs.green.expr.Expression	visit(IfThenElseExpr expr)
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

findStackSlotsOnly

private final boolean findStackSlotsOnly

symbolTable

private final com.ibm.wala.ssa.SymbolTable symbolTable

stackSlotNotFound

public boolean stackSlotNotFound

noStackSlotVars

public java.util.HashSet<WalaVarExpr> noStackSlotVars

isSymCondition

private boolean isSymCondition

foundWalaVarExpr

private boolean foundWalaVarExpr

slotParamTable

private SlotParamTable slotParamTable

sf

private gov.nasa.jpf.vm.StackFrame sf

eva

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

Constructor Detail

SymbCondVisitor

public SymbCondVisitor(gov.nasa.jpf.vm.StackFrame sf,
                       SlotParamTable slotParamTable,
                       boolean findStackSlotsOnly,
                       com.ibm.wala.ssa.SymbolTable symbolTable)

Method Detail

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(GammaVarExpr 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(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(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>

visit

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

Specified by:

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

isSymCondition

public boolean isSymCondition()

isFoundWalaVarExpr

public boolean isFoundWalaVarExpr()

execute

public static java.util.HashSet<WalaVarExpr> execute(com.ibm.wala.ssa.IR ir,
                                                     SlotParamTable slotParamTable,
                                                     Stmt staticStmt)