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

R

reason - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt

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

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

ref - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRef

ref - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef

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

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

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

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

An interface that represents a region.

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

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

region - Variable in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator

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

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

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

RegionBoundaryOutput(ArrayList<Integer>, ExprBoundaryVisitor) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryOutput

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

The visitor explores the boundaries of the region by identifying: first def, last def and first use vars.

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

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

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

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

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

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

RegionHitExactHeuristic(String, Instruction, MethodInfo, int) - Constructor for class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionHitExactHeuristic

regionHitExactHeuristicArray - Static variable in class gov.nasa.jpf.symbc.veritesting.Heuristics.HeuristicManager

used to collect all regions that we hit along with the number of paths that SPF had to explore through it.

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

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

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

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

regionKeys - Variable in class gov.nasa.jpf.symbc.VeritestingListener

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

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

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

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

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

RegionStatistics(String, FailEntry, int, int, int) - Constructor for class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionStatistics

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

This holds the region greeen expression after all transformations are done.

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

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

remaining - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode

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

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

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

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

Basic remove element/row inside the table.

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

Basic remove element/row inside the table.

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

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

RemoveEarlyReturns - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns

This class removes early return statements.

RemoveEarlyReturns() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns

RemoveEarlyReturns(StaticRegion) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns

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

RemoveEarlyReturns.ReturnResult - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns

reset() - Static method in class gov.nasa.jpf.symbc.Observations

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

reset(LinkedHashSet<Expression>) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor

resetChange() - Static method in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

resetIteration() - Static method in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

resetWrapper() - Static method in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

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

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

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

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

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

returnExp - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SimplifyGreenVisitor

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

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

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

ReturnInstruction(SSAReturnInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.ReturnInstruction

ReturnLessVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns

ReturnLessVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor

ReturnResult(Stmt, Expression, Expression, Pair<Integer, String>, Expression) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns.ReturnResult

ReturnResult(Stmt) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns.ReturnResult

ReturnResult(Stmt, RemoveEarlyReturns.ReturnResult) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns.ReturnResult

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

reverseLookup(CloneableVariable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicOutputTable

reverseLookup(int[]) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicTable

rhs - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.AssignmentStmt

rhs - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.PhiInstruction

rhs - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.ReturnInstruction

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

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

runOnSamePath(ThreadInfo, Instruction, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

runReturnSamePath(ThreadInfo, Instruction, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

runStartTime - Variable in class gov.nasa.jpf.symbc.VeritestingListener

runVeritesting(ThreadInfo, Instruction, StaticRegion, String) - Method in class gov.nasa.jpf.symbc.VeritestingListener

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

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

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