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

P

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

Base class that this used to pair any two types.

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

parametersAsString(Method) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ReflectUtil

params - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.InvokeInstruction

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

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

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

PathStatus - Enum in gov.nasa.jpf.symbc.veritesting.Heuristics

PathStatus() - Constructor for enum gov.nasa.jpf.symbc.veritesting.Heuristics.PathStatus

pathSubscript - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubscriptPair

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

pcChoiceOptimization - Variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

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

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

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

Used to throw Static Region Exception.

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

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

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

This represents a phi condition, that associates a "condition" with the "then" and the "else side.

PhiCondition(PhiCondition.Branch, Expression) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiCondition

PhiCondition.Branch - Enum in gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst

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

This is used to represent an edge from one block to another in the CFG.

PhiEdge(ISSABasicBlock, ISSABasicBlock) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiEdge

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

This is PhiInstruction in Ranger IR that matches the corresponding PhiInstruction in Wala.

PhiInstruction(SSAPhiInstruction, Expression, Expression[]) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.PhiInstruction

PhiInstruction(SSAPhiInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.PhiInstruction

populateArrayOutputs(ThreadInfo, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.VeritestingListener

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

populateFieldOutputs(ThreadInfo, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.VeritestingListener

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

populateParam() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

populateSlots(ThreadInfo, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.VeritestingListener

Populates SPF stack slot with the output of the veritesting region.

populateSlotsForVars(int, int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

populateVars(SSAInstruction, int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

This method is used only to get the stack slot of "use" vars, which are either already defined in a previous "def" and so it will be in the stackSlotMap.

populateVars(SSAInstruction, int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

postVisit(Operation) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SimplifyGreenVisitor

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

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

preprocesOnly - Static variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

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

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

Pretty print of all statements and expressions in RangerIR.

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

PrettyPrintVisitor.PrettyPrintExpr - Class in gov.nasa.jpf.symbc.veritesting.ast.visitors

print() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySubscriptMap

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

print() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.CloneableVarTable

Basic print of the table.

print() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.InputTable

print() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable

print() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

print() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table

Basic print of the table.

print() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.VarTypeTable

print() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSubscriptMap

print() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.GlobalSubscriptMap

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

print(Ast) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

print(Expression) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

print(Ast) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor

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

print() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionStatistics

printAccumulativeStatistics() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

printAllExceptionStatistics() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

printAllRegionStatistics() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

printBlock(ISSABasicBlock) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil

printBlocksUpTo(SSACFG, int) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil

printHeuristicStatistics() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

printInstantiationStatistics() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

printMethodSummary(PrintWriter, SymbolicListener.MethodSummary) - Method in class gov.nasa.jpf.symbc.SymbolicListener

printMethodSummaryHTML(PrintWriter, SymbolicListener.MethodSummary) - Method in class gov.nasa.jpf.symbc.SymbolicListener

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

printStaticAnalysisStatistics() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

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

propagateTypes(DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.TypePropagationVisitor

propertyViolated(Search) - Method in class gov.nasa.jpf.symbc.SymbolicListener

propertyViolated(Search) - Method in class gov.nasa.jpf.symbc.SymbolicListener2

psm - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.GetInstruction

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

Holds path subscript map for field references in the region

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

publishFinished(Publisher) - Method in class gov.nasa.jpf.symbc.SymbolicListener

publishFinished(Publisher) - Method in class gov.nasa.jpf.symbc.VeritestingListener

pushExpOnStack(DynamicRegion, StackFrame, String, Expression) - Static method in class gov.nasa.jpf.symbc.VeritestingListener

pushReturnOnStack(StackFrame, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.VeritestingListener

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

This is PutInstruction in RangerIR that matches the corresponding PutInstruction in Wala and subsequently the corresponding instructions in Java Bytecode.

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

PutInstruction(SSAPutInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.PutInstruction

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