- 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
-