A B C D E F G H I J K L M N O P R S T U V W Z

V

val - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.CheckCastInstruction

val - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.InstanceOfInstruction

ValidGreenPredicate - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants

This class is used to check the invariant that after AstToGreen translation, that the result is a valid Green expression that does not have IfThenElseExpr, WalaVarExpr, FieldRefVarExpr or GammaVarExpr.

ValidGreenPredicate() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.ValidGreenPredicate

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt.SPFReason

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesInstruction

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.DefUseVisit

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiCondition.Branch

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator.Kind

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.FixedPointWrapper.Transformation

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.Heuristics.PathStatus

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.StaticRegionException.ExceptionPhase

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil.SatResult

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.veritesting.VeritestingUtil.FailEntry.FailReason

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum gov.nasa.jpf.symbc.VeritestingListener.VeritestingMode

Returns the enum constant of this type with the specified name.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt.SPFReason

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesInstruction

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.DefUseVisit

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiCondition.Branch

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator.Kind

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.FixedPointWrapper.Transformation

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.Heuristics.PathStatus

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.StaticRegionException.ExceptionPhase

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil.SatResult

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.veritesting.VeritestingUtil.FailEntry.FailReason

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum gov.nasa.jpf.symbc.VeritestingListener.VeritestingMode

Returns an array containing the constants of this enum type, in the order they are declared.

ValueSymbolTable - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment

SH: This table contains the values for the region input and the constant wala variables.

ValueSymbolTable() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.ValueSymbolTable

valueSymbolTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor

varId - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRefVarExpr

varId - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRefVarExpr

varTypeTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

varTypeTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion

An environment table that holds the types of all Wala vars in the region.

varTypeTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

VarTypeTable - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment

An environment table that holds all vars to types.

VarTypeTable(IR) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.VarTypeTable

Constructor that is used to generate the type table for a method region.

VarTypeTable(IR, Pair<Integer, Integer>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.VarTypeTable

Constructor that is used to generate the type table for a conditional region, by specifying the boundaries of variables inside the region.

VarTypeTable() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.VarTypeTable

Default constructor.

varTypeTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion

An environment table that holds the types of local variables defined inside the region.

varTypeTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.ExprTypeVisitor

varTypeTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.TypePropagationVisitor

veriHitNumber - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionStatistics

counts the number of times we successfully summaries a veritesting region and placing it on the PC was SAT

veriRegions - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain

veriStatement - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

veriStatement - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

A translated RangerIR statement.

VeritestingListener - Class in gov.nasa.jpf.symbc

This is the entry point to Java Ranger.

VeritestingListener(Config, JPF) - Constructor for class gov.nasa.jpf.symbc.VeritestingListener

VeritestingListener.VeritestingMode - Enum in gov.nasa.jpf.symbc

VeritestingMain - Class in gov.nasa.jpf.symbc.veritesting

Main class file for veritesting static analysis exploration.

VeritestingMain(ThreadInfo) - Constructor for class gov.nasa.jpf.symbc.veritesting.VeritestingMain

veritestingMain - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.JITAnalysis

veritestingMode - Static variable in class gov.nasa.jpf.symbc.VeritestingListener

VeritestingMode() - Constructor for enum gov.nasa.jpf.symbc.VeritestingListener.VeritestingMode

veritestingRegions - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions

veritestingRunning - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

veritestRegionCount - Static variable in class gov.nasa.jpf.symbc.VeritestingListener

veritestRegionExpectedCount - Static variable in class gov.nasa.jpf.symbc.VeritestingListener

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

Translating a GammaExpression into an IfThenElseExpression

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

Translating a TfThenElseExpr into an IfThenElseExpression

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(IntConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(IntVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(RealConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(RealVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(StringConstantGreen) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(StringVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor

visit(IntConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(IntVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(RealConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(RealVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(StringConstantGreen) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(StringVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

visit(IntVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

visit(RealVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

visit(StringVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FirstITEStmtVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FirstITEStmtVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FirstITEStmtVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldAccessVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldAccessVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.ValidGreenPredicate

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.ValidGreenPredicate

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.ValidGreenPredicate

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.ValidGreenPredicate

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.linearization.LinearizationVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

Used to collect the predicate under which an SPFCase needs to occur.

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(IntConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(IntVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(RealConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(RealVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(StringConstantGreen) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(StringVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprBoundaryVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprRegionInputVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

While visiting IfThenElse, it is responsible for resetting the spfCasePath, if on one path of its branches an SPFCase instruction was discoverd, such as throw or object creation, if this happens then along that path, there should be no high order regions inlined.

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

Visits an InvokeInstruction by attempting to inline static method regions.

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.ExprTypeVisitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.ExprTypeVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.TypePropagationVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.ExpUniqueVisitor

A visit to all WalaVariables to create a new-unique object for the same var number.

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.ExpUniqueVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.ExpUniqueVisitor

A visit to all FieldRefVarExpr to create a new-unique object for the same var number.

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.ExpUniqueVisitor

A visit to all ArrayRefVarExpr to create a new-unique object for the same var number.

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit(AssignmentStmt) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(CompositionStmt) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(IfThenElseStmt) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(SkipStmt) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(SPFCaseStmt) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(ArrayLoadInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(ArrayStoreInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(SwitchInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(ReturnInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(GetInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(PutInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(NewInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(InvokeInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(ArrayLengthInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(ThrowInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(CheckCastInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(InstanceOfInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(PhiInstruction) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor

visit(IntConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(IntVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(RealConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(RealVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(StringConstantGreen) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(StringVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

visit(IntConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(IntVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(RealConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(RealVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(StringConstantGreen) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(StringVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

visit(IntConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(IntVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(RealConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(RealVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(StringConstantGreen) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(StringVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit(IntConstant) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(IntVariable) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(Operation) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(RealConstant) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(RealVariable) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(StringConstantGreen) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(StringVariable) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(IfThenElseExpr) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(ArrayRefVarExpr) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(WalaVarExpr) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(FieldRefVarExpr) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(GammaVarExpr) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(AstVarExpr) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(IntConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(IntVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(RealConstant) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(RealVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(StringConstantGreen) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(StringVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr

visit(AssignmentStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(SkipStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(SPFCaseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

visit(SwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(ReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(GetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(PutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(NewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(ArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(ArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(ArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(ThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(CheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(InstanceOfInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(PhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

visit(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor

visit(IfThenElseStmt) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor

visit(WalaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(FieldRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(GammaVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(IntConstant) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(IntVariable) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(AstVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(RealConstant) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(RealVariable) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(StringConstantGreen) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(StringVariable) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visit(IfThenElseExpr) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

visitArrayLength(SSAArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitArrayLength(SSAArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR array length instruction out of SSA array length instruction.

visitArrayLength(SSAArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitArrayLength(SSAArrayLengthInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitArrayLoad(SSAArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitArrayLoad(SSAArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Create an ArrayLoad Instruction in RangerIR.

visitArrayLoad(SSAArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitArrayLoad(SSAArrayLoadInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitArrayStore(SSAArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitArrayStore(SSAArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Create an ArrayStore Instruction in RangerIR.

visitArrayStore(SSAArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitArrayStore(SSAArrayStoreInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitBinaryOp(SSABinaryOpInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitBinaryOp(SSABinaryOpInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Create an Assignment Statement in RangerIR for binary operations in Wala.

visitBinaryOp(SSABinaryOpInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitBinaryOp(SSABinaryOpInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitCheckCast(SSACheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitCheckCast(SSACheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR check cast instruction out of SSA check cast instruction.

visitCheckCast(SSACheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitCheckCast(SSACheckCastInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitComparison(SSAComparisonInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitComparison(SSAComparisonInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Translates a comparision instruction in Wala SSA to RangerIR assignment statement.

visitComparison(SSAComparisonInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitComparison(SSAComparisonInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitConditionalBranch(SSAConditionalBranchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitConditionalBranch(SSAConditionalBranchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

visitConditionalBranch(SSAConditionalBranchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitConditionalBranch(SSAConditionalBranchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitConversion(SSAConversionInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitConversion(SSAConversionInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Casts in SPF involving object creation are beyond what we can support currently in Static regions, else emulate the type casting between primitive types

visitConversion(SSAConversionInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitConversion(SSAConversionInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitedBlocks - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions

For memoization, so we don't visit the same blocks over and over.

visitGet(SSAGetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitGet(SSAGetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR get instruction out of SSA get instruction.

visitGet(SSAGetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitGet(SSAGetInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitGetCaughtException(SSAGetCaughtExceptionInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitGetCaughtException(SSAGetCaughtExceptionInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

RangerIR does not support getCaughtException.

visitGetCaughtException(SSAGetCaughtExceptionInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitGetCaughtException(SSAGetCaughtExceptionInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitGoto(SSAGotoInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitGoto(SSAGotoInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Goto instructions are not translated to RangerIR and therefore should not be visited by this visitor.

visitGoto(SSAGotoInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitGoto(SSAGotoInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitInstanceof(SSAInstanceofInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitInstanceof(SSAInstanceofInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR instance of instruction out of SSA instance of instruction.

visitInstanceof(SSAInstanceofInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitInstanceof(SSAInstanceofInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitInvoke(SSAInvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitInvoke(SSAInvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR invoke instruction out of SSA invoke instruction.

visitInvoke(SSAInvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitInvoke(SSAInvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitLoadMetadata(SSALoadMetadataInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitLoadMetadata(SSALoadMetadataInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

RangerIR does not support SSALoadMeta data instruction.

visitLoadMetadata(SSALoadMetadataInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitLoadMetadata(SSALoadMetadataInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitMonitor(SSAMonitorInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitMonitor(SSAMonitorInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

RangerIR currently does not support SSAMonitor instructions.

visitMonitor(SSAMonitorInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitMonitor(SSAMonitorInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitNew(SSANewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitNew(SSANewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR new instruction out of SSA new instruction.

visitNew(SSANewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitNew(SSANewInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitPhi(SSAPhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitPhi(SSAPhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR phi instruction out of Wala's phi instruction.

visitPhi(SSAPhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitPhi(SSAPhiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitPi(SSAPiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitPi(SSAPiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Ranger IR does not need to support Wala's Pi instruction.

visitPi(SSAPiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitPi(SSAPiInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitPut(SSAPutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitPut(SSAPutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR put instruction out of SSA put instruction.

visitPut(SSAPutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitPut(SSAPutInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitReturn(SSAReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitReturn(SSAReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR return instruction out of SSA return instruction.

visitReturn(SSAReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitReturn(SSAReturnInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitSwitch(SSASwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitSwitch(SSASwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

RangerIR currently does not support Switch instruction.

visitSwitch(SSASwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitSwitch(SSASwitchInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitThrow(SSAThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitThrow(SSAThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Creates RangerIR throw instruction out of SSA throw instruction.

visitThrow(SSAThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitThrow(SSAThrowInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

visitUnaryOp(SSAUnaryOpInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

visitUnaryOp(SSAUnaryOpInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Translates a unary instruction in Wala SSA to RangerIR assignment statement.

visitUnaryOp(SSAUnaryOpInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

visitUnaryOp(SSAUnaryOpInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

A B C D E F G H I J K L M N O P R S T U V W Z