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

S

s1 - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.CompositionStmt

s2 - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.CompositionStmt

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

SamePathOptimization - Class in gov.nasa.jpf.symbc.veritesting.ChoiceGenerator

SamePathOptimization() - Constructor for class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

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

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

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

searchFinished(Search) - Method in class gov.nasa.jpf.symbc.GreenListener

second - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.Pair

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

seenBiggerWalaNum(int, int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprRegionInputVisitor

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

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

seenSlots - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprRegionInputVisitor

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

setArgTypes(String) - Method in class gov.nasa.jpf.symbc.SymbolicListener.MethodSummary

setArgValues(String) - Method in class gov.nasa.jpf.symbc.SymbolicListener.MethodSummary

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

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

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

setMethodName(String) - Method in class gov.nasa.jpf.symbc.SymbolicListener.MethodSummary

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

setSymValues(String) - Method in class gov.nasa.jpf.symbc.SymbolicListener.MethodSummary

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

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

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

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

This populates the Output of the summarized region to SPF.

setValueSymbolTable(DynamicTable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor

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

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

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

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

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

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

SimplifyRangerExprVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop

SimplifyRangerExprVisitor(DynamicTable<Expression>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor

SimplifyStmtVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop

SimplifyStmtVisitor(DynamicRegion, DynamicTable<Expression>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor

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

skip - Static variable in class gov.nasa.jpf.symbc.veritesting.ast.def.SkipStmt

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

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

A Skip statement in RangerIR.

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

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

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

A table that holds the mapping of vars in the dynamic statement to their corresponding stack slot.

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

This is the basic table, on which the input and output of the region are defined.

SlotParamTable(IR, Boolean, Stmt) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

SlotParamTable(IR, Boolean, Stmt, Pair<Integer, Integer>, int, int) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

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

slotParamTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

slotParamTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

slotParamTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprRegionInputVisitor

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

An Environment table that holds a mapping from vars to either their stack slot position, in case of conditional regions, or to their parameter number in case of a MethodRegion.

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

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

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

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

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

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

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

somethingChanged - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor

This is used to capture the fact that there is change happening in the transformation, this is used for the quick check for the fix point computation.

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

Holds all SPFCases predicates that are not statically summarized and are left for SPF to explore.

SPFCaseList - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases

SPFCaseList(LinkedHashSet<SPFCaseStmt>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SPFCaseList

SPFCaseList() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SPFCaseList

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

This is used to identify if a path had spfCase instruction that requires prouning the path.

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

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

SpfCasesInstruction - Enum in gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases

This is the first pass of SPFCases that creates SPFCases nodes.

SpfCasesInstruction() - Constructor for enum gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesInstruction

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

SpfCasesPass1Visitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases

SpfCasesPass1Visitor(ThreadInfo, ArrayList) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor

SpfCasesPass2Visitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases

This is the second pass of the SPFCases where the SPFCases nodes are eliminated and instead the dynamic region is populated with the predicates for the SPFCases.

SpfCasesPass2Visitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

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

This is SPFCases in RangerIR.

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

SPFCaseStmt.SPFReason - Enum in gov.nasa.jpf.symbc.veritesting.ast.def

These are the different reasons that requires SPF exploration.

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

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

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

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

counts the number of times we couldn't veritest a region and we left it for SPF to deal with it.

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

This carries the green expression under which partial evaluation will be done with SPF.

SPFReason() - Constructor for enum gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt.SPFReason

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

Translates an SPF expression to a Green Expression.

SpfToGreenExprVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases

SpfToGreenExprVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor

SpfToGreenVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases

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

SpfToGreenVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor

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

This class provides some utility methods for SPF.

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

sre - Static variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

sre - Static variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor

sre - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.ExpUniqueVisitor

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

SSAToStatDefVisitor(IR, HashSet<WalaVarExpr>, SlotParamTable) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

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

This visitor translates specific Wala SSAInstructions to RangerIR.

SSAToStatIVisitor(IR, ISSABasicBlock, Map<PhiEdge, List<PhiCondition>>, Deque<PhiCondition>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

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

Some utility methods used during construction of the StaticRegion.

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

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

Holds the expression that should be written out to the stack

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

Holds the expression that should be written out to the stack

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

This visitor fills the stack slots for wala vars.

StackSlotIVisitor(IR, SlotParamTable) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

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

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

This tries to infer the stack slots for phi "def" vars and phi "use" vars by either figuring out the stack slots of one "use" var and populate it to be for the phi "def" var, or the opposite, that is the stack slot of the phi "def" was known and so it is propagated to the "use" vars

startAnalysis(String, String, String) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingMain

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

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

stateAdvanced(Search) - Method in class gov.nasa.jpf.symbc.HeuristicListener

stateAdvanced(Search) - Method in class gov.nasa.jpf.symbc.VeritestingListener

stateBacktracked(Search) - Method in class gov.nasa.jpf.symbc.VeritestingListener

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

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

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

staticAnalysisComplete() - Static method in exception gov.nasa.jpf.symbc.veritesting.StaticRegionException

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

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

StaticBranchChoiceGenerator - Class in gov.nasa.jpf.symbc.veritesting.ChoiceGenerator

StaticBranchChoiceGenerator(DynamicRegion, Instruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator

StaticBranchChoiceGenerator(DynamicRegion, Instruction, boolean) - Constructor for class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator

StaticPCChoiceGenerator - Class in gov.nasa.jpf.symbc.veritesting.ChoiceGenerator

StaticPCChoiceGenerator(int, DynamicRegion, Instruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator

StaticPCChoiceGenerator.Kind - Enum in gov.nasa.jpf.symbc.veritesting.ChoiceGenerator

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

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

A class that represents a Static Region.

StaticRegion(Stmt, IR, Boolean, int, ISSABasicBlock, ISSABasicBlock, RemoveEarlyReturns.ReturnResult) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion

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

staticRegionException - Static variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode

StaticRegionException - Exception in gov.nasa.jpf.symbc.veritesting

Exception class used whenever violation was detected during veritesting.

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

StaticRegionException.ExceptionPhase - Enum in gov.nasa.jpf.symbc.veritesting

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

Statement of the region.

StaticTable<V> - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment

Base class for all environment tables.

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

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

This visitor fills types for wala vars, by using Wala Type inference.

StaticTypeIVisitor(IR, VarTypeTable, Pair<Integer, Integer>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

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

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

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

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

Defines an interface for all statements in the RangerIR.

stmt - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

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

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

stmtList - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor

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

Prints out Statement in RangerIR.

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

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

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

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

subscript - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRefVarExpr

SubscriptPair - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess

SubscriptPair(Integer, Integer) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubscriptPair

substituteGet(GetInstruction, FieldRef) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor

SubstituteGetOutput - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess

SubstituteGetOutput(ThreadInfo, FieldRef, boolean, Expression) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput

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

The Substitution Transformation is responsible for replacing all vars with their symbolic values if found, as well as the substitution of all constant vars.

SubstitutionVisitor(ThreadInfo, DynamicRegion, DynamicTable, boolean, ArrayList<MethodReference>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

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

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

SwitchInstruction(SSASwitchInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.SwitchInstruction

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

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

Visits expression in a conditional statement to check if any of its arguments are indeed symbolic.

SymbCondVisitor(StackFrame, SlotParamTable, boolean, SymbolTable) - Constructor for class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

SymbolicInstructionFactory - Class in gov.nasa.jpf.symbc

SymbolicInstructionFactory(Config) - Constructor for class gov.nasa.jpf.symbc.SymbolicInstructionFactory

SymbolicListener - Class in gov.nasa.jpf.symbc

SymbolicListener(Config, JPF) - Constructor for class gov.nasa.jpf.symbc.SymbolicListener

SymbolicListener.MethodSummary - Class in gov.nasa.jpf.symbc

SymbolicListener2 - Class in gov.nasa.jpf.symbc

SymbolicListener2(Config, JPF, BlockingQueue<Pair<PathCondition, Map<String, Object>>>) - Constructor for class gov.nasa.jpf.symbc.SymbolicListener2

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

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

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