- f2d() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- f2i() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- f2l() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- fadd() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- FailEntry - Class in gov.nasa.jpf.symbc.veritesting.VeritestingUtil
-
- FailEntry(FailEntry.FailReason, String) - Constructor for class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.FailEntry
-
- FailEntry.FailReason - Enum in gov.nasa.jpf.symbc.veritesting.VeritestingUtil
-
- failMsg - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.FailEntry
-
- failReason - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.FailEntry
-
- FailReason() - Constructor for enum gov.nasa.jpf.symbc.veritesting.VeritestingUtil.FailEntry.FailReason
-
- failReasonList - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionStatistics
-
- failures - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.ValidGreenPredicate
-
- faload() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- fastore() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- fcmpg() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- fcmpl() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- fdiv() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- field - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef
-
- field - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.GetInstruction
-
- field - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.PutInstruction
-
- FIELD_SUBSCRIPT_BASE - Static variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor
-
- FieldAccessVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess
-
- FieldAccessVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldAccessVisitor
-
- FieldArrayVarToSPFVarVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen
-
A visitor that visits all FieldRefVarExpr and generates the appropriate SPF symbolic variable based on its type.
- FieldArrayVarToSPFVarVisitor(FieldRefTypeTable) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor
-
- fieldExceptionNumber - Static variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor
-
- FieldRef - Class in gov.nasa.jpf.symbc.veritesting.ast.def
-
This class is used to represent field-reference pair that is used in RangerIR to provide SSA for fields.
- FieldRef(int, String, String, boolean) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef
-
- fieldRef - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRefVarExpr
-
- fieldRef - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput
-
- fieldRefTypeTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor
-
- fieldRefTypeTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion
-
An environment table that holds the types of all field variables, referenced by FieldRefVarExpr objects, in the region.
- FieldRefTypeTable - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment
-
An environment table that maps FieldRefVarExpr (field expressions) to types.
- FieldRefTypeTable() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FieldRefTypeTable
-
Default constructor.
- FieldRefTypeTable(int) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FieldRefTypeTable
-
- FieldRefVarExpr - Class in gov.nasa.jpf.symbc.veritesting.ast.def
-
A class that carries a fieldReference with a specific SSA subscript.
- FieldRefVarExpr(FieldRef, SubscriptPair) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRefVarExpr
-
- FieldRefVarExpr(FieldRef, SubscriptPair, int) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRefVarExpr
-
- FieldSSAVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess
-
- FieldSSAVisitor(ThreadInfo, DynamicRegion) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor
-
- FieldSubscriptMap - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess
-
- FieldSubscriptMap() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSubscriptMap
-
- fillValueSymbolTable(ThreadInfo, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor
-
Fills out the values of all vars that could be discovered in the region.
- filter - Variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- filterTable(Pair<Integer, Integer>, ArrayList<Integer>, HashSet<Integer>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable
-
- finalValue - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput
-
- findAllReturns(IR) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable
-
- findClasses(ThreadInfo, ClassHierarchy, ArrayList<String>, String, HashSet<String>) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
-
- findClasses(ThreadInfo, ClassHierarchy, String, String, HashSet<String>) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ClassUtils
-
- findCommonSuccessor(ISSABasicBlock) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode
-
This attempts to walk all successors of a block to try to find the end block node.
- findConditionalSuccessors(ISSABasicBlock, ISSABasicBlock) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
-
Attempts to discover conditional successors on the then or the else side of a conditional block.
- findLastVar(Integer, Integer, Integer, Integer) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion
-
- findMethodRegion(ThreadInfo, InvokeInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor
-
Attempts to find a mapping MethodRegion.
- findMinConvergingNode() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode
-
Finds the end block of a region.
- findSelfContainedSubgraphs(ISSABasicBlock, ISSABasicBlock, ISSABasicBlock, Set<ISSABasicBlock>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
-
This searches a self contained subgraph inside the region.
- findStackSlotsOnly - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor
-
- FindStructuredBlockEndNode - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst
-
Attempts to discover end node of a region, by walking successors of presumably a block that ends with a conditional instruction.
- FindStructuredBlockEndNode(SSACFG, ISSABasicBlock, ISSABasicBlock) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode
-
- first - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.Pair
-
- first - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.Triple
-
- firstException - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor
-
this is used when computing fixed point to carry the first exception that the visitor might have encountered.
- firstException - Static variable in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper
-
Keeps the first exception that has been encountered in all the transformations.
- FirstITEStmtVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment
-
- FirstITEStmtVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FirstITEStmtVisitor
-
- firstTime - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.JITAnalysis
-
- firstUse - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor
-
- firstUse - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprBoundaryVisitor
-
- FixedPointAstMapVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.visitors
-
- FixedPointAstMapVisitor(ExprVisitor<Expression>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor
-
- fixedPointTime - Static variable in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper
-
- FixedPointWrapper - Class in gov.nasa.jpf.symbc.veritesting
-
This class is called multiple times over different transformations.
- FixedPointWrapper() - Constructor for class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper
-
- FixedPointWrapper.Transformation - Enum in gov.nasa.jpf.symbc.veritesting
-
- flattenStmt(Stmt) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor
-
- FlattenStmtListVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns
-
This class flattens statement lists like ((s1; s2); (s3; s4)) into a "flat" list like: (s1; (s2; (s3; s4)))).
- FlattenStmtListVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor
-
- fmul() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- fneg() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- foldBooleanOp(Operation) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil
-
- ForallAstVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.visitors
-
- ForallAstVisitor(ForallExprVisitor) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.visitors.ForallAstVisitor
-
Visits all statements for checking invariants over statements.
- ForallExprVisitor - Class in gov.nasa.jpf.symbc.veritesting.ast.visitors
-
A visitor that enforces invariant checking on all expressions by passing the operation and expected result.
- ForallExprVisitor() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.visitors.ForallExprVisitor
-
- formatString - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionHitExactHeuristic
-
- foundStoppingInsn - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor
-
- foundWalaVarExpr - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor
-
- fp - Static variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- frem() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- from - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiEdge
-
- fsub() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-