public class SpfCasesPass1Visitor extends java.lang.Object implements AstVisitor<Stmt>
| Modifier and Type | Field and Description |
|---|---|
private java.util.ArrayList<SpfCasesInstruction> |
spfCasesInstructionList |
private za.ac.sun.cs.green.expr.Expression |
spfCondition |
private gov.nasa.jpf.vm.ThreadInfo |
ti |
| Constructor and Description |
|---|
SpfCasesPass1Visitor(gov.nasa.jpf.vm.ThreadInfo ti,
java.util.ArrayList spfCasesInstructionList) |
| Modifier and Type | Method and Description |
|---|---|
private za.ac.sun.cs.green.expr.Expression |
createArrayCondition(ArrayRefVarExpr arrayRefVarExpr) |
static DynamicRegion |
execute(gov.nasa.jpf.vm.ThreadInfo ti,
DynamicRegion dynRegion,
java.util.ArrayList spfCasesInstructionList) |
Stmt |
visit(ArrayLengthInstruction c) |
Stmt |
visit(ArrayLoadInstruction c) |
Stmt |
visit(ArrayStoreInstruction c) |
Stmt |
visit(AssignmentStmt a) |
Stmt |
visit(CheckCastInstruction c) |
Stmt |
visit(CompositionStmt a) |
Stmt |
visit(GetInstruction c) |
Stmt |
visit(IfThenElseStmt a)
Used to collect the predicate under which an SPFCase needs to occur.
|
Stmt |
visit(InstanceOfInstruction c) |
Stmt |
visit(InvokeInstruction c) |
Stmt |
visit(NewInstruction c) |
Stmt |
visit(PhiInstruction c) |
Stmt |
visit(PutInstruction c) |
Stmt |
visit(ReturnInstruction c) |
Stmt |
visit(SkipStmt a) |
Stmt |
visit(SPFCaseStmt c) |
Stmt |
visit(SwitchInstruction c) |
Stmt |
visit(ThrowInstruction c) |
private za.ac.sun.cs.green.expr.Expression spfCondition
private gov.nasa.jpf.vm.ThreadInfo ti
private java.util.ArrayList<SpfCasesInstruction> spfCasesInstructionList
public SpfCasesPass1Visitor(gov.nasa.jpf.vm.ThreadInfo ti,
java.util.ArrayList spfCasesInstructionList)
public Stmt visit(AssignmentStmt a)
visit in interface AstVisitor<Stmt>private za.ac.sun.cs.green.expr.Expression createArrayCondition(ArrayRefVarExpr arrayRefVarExpr)
public Stmt visit(CompositionStmt a)
visit in interface AstVisitor<Stmt>public Stmt visit(IfThenElseStmt a)
visit in interface AstVisitor<Stmt>public Stmt visit(SkipStmt a)
visit in interface AstVisitor<Stmt>public Stmt visit(SPFCaseStmt c)
visit in interface AstVisitor<Stmt>public Stmt visit(ArrayLoadInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(ArrayStoreInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(SwitchInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(ReturnInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(GetInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(PutInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(NewInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(InvokeInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(ArrayLengthInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(ThrowInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(CheckCastInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(InstanceOfInstruction c)
visit in interface AstVisitor<Stmt>public Stmt visit(PhiInstruction c)
visit in interface AstVisitor<Stmt>public static DynamicRegion execute(gov.nasa.jpf.vm.ThreadInfo ti, DynamicRegion dynRegion, java.util.ArrayList spfCasesInstructionList)