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

A

aaload() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

aastore() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLengthInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLoadInstruction

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

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayStoreInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.AssignmentStmt

accept(AstVisitor<T>) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.def.Ast

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

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.CheckCastInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.CompositionStmt

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

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

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.GetInstruction

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

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseStmt

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.InstanceOfInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.InvokeInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.NewInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.PhiInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.PutInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ReturnInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.SkipStmt

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt

accept(AstVisitor<T>) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.def.Stmt

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.SwitchInstruction

accept(AstVisitor<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ThrowInstruction

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

accept(Expression) - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitorAdapter

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

add(Integer, Pair<Expression[], String>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayExpressions

add(ArrayRef, SubscriptPair) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySubscriptMap

add(Integer, Integer) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.GlobalArraySubscriptMap

add(CloneableVariable, T) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.CloneableVarTable

Basic add row inside the table.

add(K, V) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table

Basic add row inside the table.

add(FieldRef, SubscriptPair) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSubscriptMap

add(FieldRef, Integer) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.GlobalSubscriptMap

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

addAll(DynamicTable<V>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicTable

addAll(SPFCaseList) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SPFCaseList

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

addPathCondition(Pair) - Method in class gov.nasa.jpf.symbc.SymbolicListener.MethodSummary

addRegionExactHeuristic(RegionHitExactHeuristic) - Static method in class gov.nasa.jpf.symbc.veritesting.Heuristics.HeuristicManager

addSubClassNames(ThreadInfo, ClassHierarchy, HashSet<String>, String) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ClassUtils

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

adjustForDepth(List<LinkedList<PhiCondition>>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

Used to ignore the "out of scope" conditions corresponding to ancestor branches, if this is a phi is for a nested if/then/else,

advanceSpf(Instruction, DynamicRegion, boolean) - Static method in class gov.nasa.jpf.symbc.VeritestingListener

Steps SPF to the end of the region.

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

allDefs - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor

allSummaries - Variable in class gov.nasa.jpf.symbc.SymbolicListener

allUses - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprBoundaryVisitor

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

aload_0() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

aload_1() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

aload_2() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

aload_3() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

analyze(StaticRegion) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns

analyzeForVeritesting(ArrayList<String>, String) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingMain

anewarray(String) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

argTypes - Variable in class gov.nasa.jpf.symbc.SymbolicListener.MethodSummary

argValues - Variable in class gov.nasa.jpf.symbc.SymbolicListener.MethodSummary

ARRAY_SUBSCRIPT_BASE - Static variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

arrayExceptionNumber - Static variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

ArrayExpressions - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess

ArrayExpressions(ThreadInfo) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayExpressions

ArrayExpressions(ThreadInfo, HashMap, HashMap) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayExpressions

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

arraylength() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

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

This is ArrayLengthInstruction in RangerIR that matches the corresponding ArrayLengthInstruction in Wala and subsequently the instruction in Java Bytecode.

ArrayLengthInstruction(SSAArrayLengthInstruction, Expression, Expression) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLengthInstruction

ArrayLengthInstruction(SSAArrayLengthInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLengthInstruction

arrayLoadInsns - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FirstITEStmtVisitor

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

This is ArrayLoadInstruction in RangerIR that matches the corresponding ArrayLoadInstruction in Wala and subsequently the instruction in Java Bytecode.

ArrayLoadInstruction(SSAArrayLoadInstruction, Expression, Expression, TypeReference, Expression) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLoadInstruction

ArrayLoadInstruction(SSAArrayLoadInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLoadInstruction

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

Holds output expressions to be written into arrays

arrayref - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLengthInstruction

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

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

ArrayRef(int, Expression) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRef

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

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

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

ArrayRefVarExpr(ArrayRef, SubscriptPair) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRefVarExpr

ArrayRefVarExpr(ArrayRef, SubscriptPair, int) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRefVarExpr

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

ArraySSAVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess

ArraySSAVisitor(ThreadInfo, DynamicRegion) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

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

This is ArrayStoreInstruction in RangerIR that matches the corresponding ArrayStoreInstruction in Wala and subsequently the instruction in Java Bytecode.

ArrayStoreInstruction(SSAArrayStoreInstruction, Expression, Expression, TypeReference, Expression) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayStoreInstruction

ArrayStoreInstruction(SSAArrayStoreInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayStoreInstruction

ArraySubscriptMap - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess

ArraySubscriptMap() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySubscriptMap

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

ArrayUtil - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess

ArrayUtil() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayUtil

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

assign - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns.ReturnResult

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

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

assignExpr - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.PutInstruction

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

Assignment Statement in RangerIR.

AssignmentStmt(Expression, Expression) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.AssignmentStmt

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

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

Ast - Interface in gov.nasa.jpf.symbc.veritesting.ast.def

Interface that provides the signature of accept method which all Statements in RangerIR supports.

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

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

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

A RangerIR statement visitor that creates a new instance of the statement.

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

AstToGreenExprVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen

This is a visitor class that Translate expression in RangerIR to te appropriate Green expression.

AstToGreenExprVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

AstToGreenVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen

Main visitor that visits all statements and translate them to the appropriate green expression.

AstToGreenVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor

AstToString(Expression) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil

Pretty print method to print Green expression.

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

AstVarExpr MWW: this is the variable expression for generated local variables.

AstVarExpr(String, String) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.AstVarExpr

AstVarExpr(String, String, int) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.AstVarExpr

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

An interface for visiting all Statements in RangerIR.

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

Attempts to translate conditional region and translates it to RangerIR statement

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

keeps track of all classes we have seen for recovering of the IR

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

keeps track of all the methods we have seen for recovering the IR

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

attemptHighOrderRegion(DynamicRegion, DynamicTable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

Attempts to substitute in a high order region.

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

This methods attempt to connect discover multi-path regions and connecting them to recover the method as well.

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

Attempts to translate a method region to a RangerIR statement.

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

Translates from current block but does not include the ending block.

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

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