- main - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor
-
- makeArrayRef(ArrayLoadInstruction) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRef
-
- makeArrayRef(ArrayStoreInstruction) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRef
-
- makeClonableVarUniqueKey(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicTable
-
Appends a postfix to each key in the table.
- makeConstantFromWala(SymbolTable, int) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.WalaUtil
-
This method is used to return a Green expression for a wala var name, based on the type of the constant.
- makeConstantsTableUnique(DynamicTable<Expression>, int) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor
-
- makeGetFieldRef(ThreadInfo, GetInstruction) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef
-
- makePutFieldRef(ThreadInfo, PutInstruction) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef
-
- makeSymbolicInteger(String) - Method in class gov.nasa.jpf.symbc.VeritestingListener
-
- makeUnique(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRefVarExpr
-
- makeUnique(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.AstVarExpr
-
- makeUnique(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.CloneableVariable
-
- makeUnique(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRefVarExpr
-
- makeUnique(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.WalaVarExpr
-
- makeUnique(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayExpressions
-
- makeUniqueKey(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.CloneableVarTable
-
Appends a postfix to each key in the table.
- makeVeritestingCG(ThreadInfo, Instruction, String) - Method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator
-
- makeVeritestingCG(ThreadInfo, Instruction, String) - Method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator
-
- maxBranchDepth - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager
-
- maxDepth - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion
-
Holds the total number of IfThenElseStmts present in this static region
- maxDepth - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion
-
Holds the total number of IfThenElseStmts present in this static region
- maxDepth - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor
-
- maxExecPathCount - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager
-
- maxLimit - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode
-
- maxPcLength - Static variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- maxPcMSec - Static variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- maxStaticExplorationDepth - Static variable in class gov.nasa.jpf.symbc.VeritestingListener
-
- MaxTries - Static variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- maybeParseConstraint(PathCondition) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil
-
- mergeArrayExpressions(Expression, ArrayExpressions, ArrayExpressions) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor
-
- mergeExpressionTable(CloneableVarTable<T>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.CloneableVarTable
-
Merge the table with the entries of another table.
- mergePSM(Expression, FieldSubscriptMap, FieldSubscriptMap) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor
-
- mergeTable(StaticTable<V>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTable
-
Merge the table with the eateries of another table.
- mergeTable(Table) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table
-
Merging another table to current one.
- methodAnalysis - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
-
- methodExited(VM, ThreadInfo, MethodInfo) - Method in class gov.nasa.jpf.symbc.SymbolicListener2
-
- methodInfo - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionHitExactHeuristic
-
- methodName - Variable in class gov.nasa.jpf.symbc.SymbolicListener.MethodSummary
-
- methodSig - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
-
- MethodSummary() - Constructor for class gov.nasa.jpf.symbc.SymbolicListener.MethodSummary
-
- methodSummaryClassNames - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
-
- methodSummarySubClassNames - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
-
- minConvergingNode - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode
-
- minLimit - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode
-
- multianewarray(String, int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
-
- multiPathRegSymbolValueTable - Static variable in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper
-