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

E

earlyReturnCondition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

earlyReturnPredicate - Static variable in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

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

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

Holds the early return result that is computed by the RemoveEarlyReturns pass called in VeritestingListener

earlyReturnToGreen(Expression, DynamicRegion) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

elementType - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLoadInstruction

elementType - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayStoreInstruction

ELSE_CHOICE - Static variable in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator

elseExpr - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.GammaVarExpr

elseExpr - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseExpr

elsePredicate - Static variable in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

elseStmt - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseStmt

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

emptyFolder(File) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil

endingInsnsHash - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain

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

Identifies the End Position that the region is summarizing and which also SPF to resume from.

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

this is the last instruction where SPF needs to start from after the region

enqueue(PriorityQueue<E>, E) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil

equal(RegionHitExactHeuristic) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionHitExactHeuristic

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLengthInstruction

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLoadInstruction

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRef

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRefVarExpr

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayStoreInstruction

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.AssignmentStmt

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.AstVarExpr

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.CheckCastInstruction

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.CloneableVariable

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.CompositionStmt

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRefVarExpr

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.GammaVarExpr

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.GetInstruction

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseExpr

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseStmt

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.InstanceOfInstruction

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.InvokeInstruction

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.NewInstruction

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.PhiInstruction

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.PutInstruction

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ReturnInstruction

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.SkipStmt

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt

equals(Stmt) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.def.Stmt

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.SwitchInstruction

equals(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ThrowInstruction

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.WalaVarExpr

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubscriptPair

equals(Object) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiEdge

estimatedPathCount - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionHitExactHeuristic

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor

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

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

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

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

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

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

eva - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

exception - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

exceptionalMessage - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput

ExceptionMap - Static variable in exception gov.nasa.jpf.symbc.veritesting.StaticRegionException

ExceptionPhase(String) - Constructor for enum gov.nasa.jpf.symbc.veritesting.StaticRegionException.ExceptionPhase

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

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

execute(DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

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

execute(TransformationData) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.DefaultTransformation

execute(DynamicRegion) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.DefaultTransformation

execute(Stmt) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FirstITEStmtVisitor

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

execute(StaticRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor

execute(DynamicRegion) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.linearization.LinearizationTransformation

execute(ThreadInfo, DynamicRegion, ArrayList) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

execute(DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

This executes the second path of the SPFCases.

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

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

Executes substitution over a non-method region.

execute(TransformationData) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.transformations.Transformation

execute(TransformationData) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.TransformationList

execute(StaticRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.UniqueRegion

Used to create a unique conditional region.

execute(DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.UniqueRegion

execute() - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor

execute(ThreadInfo, Instruction, int) - Method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator

execute(ThreadInfo, Instruction, int) - Method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator

execute(StaticRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor

execute(DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor

execute(IR, SlotParamTable, Stmt) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

executeBinaryIf(Instruction, int) - Method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator

executeFixedPointHighOrder(ThreadInfo, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

executeFixedPointTransformations(ThreadInfo, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

executeInstruction(VM, ThreadInfo, Instruction) - Method in class gov.nasa.jpf.symbc.VeritestingListener

Listener's main method that checks every instruction for being a potential veritesting region.

executeNullIf(Instruction) - Method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator

executeRead(ElementInfo, FieldInfo) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput

executeUnaryIf(Instruction, int) - Method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator

executeWrite(ElementInfo, FieldInfo) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput

ExprBoundaryVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst

An Expression Boundary Visitor that attempts to discover first "use" var inside a region.

ExprBoundaryVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprBoundaryVisitor

ExprIdVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.visitors

ExprIdVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor

ExprIterVisitor<T> - Class in gov.nasa.jpf.symbc.veritesting.ast.visitors

Visits all expressions and applies the checking "combine" and returns the result of the checking.

ExprIterVisitor(BinaryOperator<T>, T) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

ExprMapVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.visitors

RangerIR expression visitor that creates a new instance of the same expression.

ExprMapVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

exprRegionInputVisitor - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor

ExprRegionInputVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst

Conditional region input visitor that visits all use vars to collect a possible first use for every stack slot.

ExprRegionInputVisitor(InputTable, SlotParamTable) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprRegionInputVisitor

ExprSubstitutionVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution

This is the expression visitor class used during substitution that either returns the value of a variable from a symbol table to returns the expression back if it doesn't make to any entry.

ExprSubstitutionVisitor(ThreadInfo, DynamicRegion, DynamicTable) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor

ExprTypeVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation

ExprTypeVisitor(DynamicTable) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.ExprTypeVisitor

ExprUtil - Class in gov.nasa.jpf.symbc.veritesting.VeritestingUtil

A utility class that provides some methods from SPF to Green and vise versa.

ExprUtil() - Constructor for class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil

ExprUtil.SatResult - Enum in gov.nasa.jpf.symbc.veritesting.VeritestingUtil

exprVisitor - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

exprVisitor - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryOutput

exprVisitor - Static variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns

exprVisitor - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

exprVisitor - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

exprVisitor - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

ExprVisitor<T> - Interface in gov.nasa.jpf.symbc.veritesting.ast.visitors

An interface for visiting all expression in RangerIR.

ExprVisitorAdapter<T> - Class in gov.nasa.jpf.symbc.veritesting.ast.visitors

An adaptor that pushes the visitor to the right visit for a Green expression.

ExprVisitorAdapter(ExprVisitor<T>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitorAdapter

ExprVisitorAdapter(EquationExprVisitor) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitorAdapter

ExpUniqueVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness

Unique Expression Visitor that ensures the uniqueness of vars used inside the region.

ExpUniqueVisitor(int) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.ExpUniqueVisitor

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

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

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