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

T

table - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayExpressions

table - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySubscriptMap

table - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.GlobalArraySubscriptMap

table - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.CloneableVarTable

Table<K,V> - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment

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

Table(String, String, String) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table

table - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table

table - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSubscriptMap

table - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.GlobalSubscriptMap

tableName - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySubscriptMap

tableName - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.GlobalArraySubscriptMap

tableName - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.CloneableVarTable

tableName - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table

tableName - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSubscriptMap

tableName - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.GlobalSubscriptMap

tableswitch(int, int, int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

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

targetMethodName - Variable in class gov.nasa.jpf.symbc.SymbolicListener2

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

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

for complex conditions, we want to record the then condition and successors.

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

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

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

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

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

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

theVisitor - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitorAdapter

third - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.Triple

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

thisNumPaths - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor

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

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

throwException(StaticRegionException, StaticRegionException.ExceptionPhase) - Static method in exception gov.nasa.jpf.symbc.veritesting.StaticRegionException

throwException(IllegalArgumentException, StaticRegionException.ExceptionPhase) - Static method in exception gov.nasa.jpf.symbc.veritesting.StaticRegionException

ThrowInstruction - Class in gov.nasa.jpf.symbc.veritesting.ast.def

This is ThrowInstruction in Ranger IR that matches the corresponding ThrowInstruction in Wala and subsequently the instruction in Java Bytecode.

ThrowInstruction(SSAThrowInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ThrowInstruction

ti - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayExpressions

ti - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

ti - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor

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

ti - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

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

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

ti - Static variable in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

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

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

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

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

to - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiEdge

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

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

toGreenSinglePredicate(SPFCaseList) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

topStackFrame - Static variable in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

toString() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayExpressions

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

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

toString() - Method in enum gov.nasa.jpf.symbc.veritesting.StaticRegionException.ExceptionPhase

toString() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.FailEntry

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

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

Holds the total number of execution paths that can be taken through this region

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

Holds the total number of execution paths that can be taken through this region

totalNumPaths - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor

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

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

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

Transformation - Interface in gov.nasa.jpf.symbc.veritesting.ast.transformations

A Transformation describes a transformation and the set of invariants that are expected to hold prior to and after its occurrence.

Transformation() - Constructor for enum gov.nasa.jpf.symbc.veritesting.FixedPointWrapper.Transformation

TransformationData - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations

Data class defining interface for invariants.

TransformationData(DynamicRegion, Set<Invariant>, boolean) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.TransformationData

TransformationList - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations

Used to iterate over all transformations, executes them and check their invariants after transformations.

TransformationList(List<Transformation>, String) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.TransformationList

transformations - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.TransformationList

translateBinaryOp(IBinaryOpInstruction.Operator) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil

Translate a binary operation to the appropriate Green operator.

translateBinaryOp(IShiftInstruction.Operator) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil

Translate a binary shift operation to the appropriate Green operator.

translateInternalBlock(ISSABasicBlock) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions

This translates "internal" blocks inside the region, these are blocks that are not the begining or the end of the region.

translateNotExpr(Operation) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil

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

Translates a phi to RangerIR assignment statement of a Gamma expression.

translateTruncatedFinalBlock(ISSABasicBlock) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions

This translate the last block in an identified region by visiting all its instructions and creating a Gamma if a Phi instruction was found.

translateUnaryOp(IUnaryOpInstruction.Operator) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil

Translates a unary operation in Wala to its corresponding Green operator.

Triple<T,V,K> - Class in gov.nasa.jpf.symbc.veritesting.VeritestingUtil

Base class that this used to pair any three types.

Triple(T, V, K) - Constructor for class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.Triple

type - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.AstVarExpr

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

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

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

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