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

C

caload() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
 
canPropagateTypeInfo(Expression, Expression) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.ExprTypeVisitor
 
canSetPC(ThreadInfo, DynamicRegion, Integer) - Static method in class gov.nasa.jpf.symbc.VeritestingListener
This method checks that the current PathCondition and after appending the summarized region is satisfiable.
canVeritest - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor
Used to indicate instructions that cannot be veritested.
casesList - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SPFCaseList
 
castore() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
 
cfg - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode
 
cfg - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
 
cha - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
 
changed - Static variable in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper
Tells if there has been a change
changedTransformation - Static variable in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper
Tells which transformation is responsible for the change, thi carries the first transformation that has happened.
CheckCastInstruction - Class in gov.nasa.jpf.symbc.veritesting.ast.def
This is CheckCastInstruction in RangerIR that matches the corresponding CheckCastInstruction in Wala and subsequently the instruction in Java Bytecode.
CheckCastInstruction(SSACheckCastInstruction, Expression, Expression, TypeReference[]) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.CheckCastInstruction
 
CheckCastInstruction(SSACheckCastInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.CheckCastInstruction
 
checkedType - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.InstanceOfInstruction
 
checkInvariant(Region) - Method in interface gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariant
 
checkInvariant(Expression, Map<Class, Integer>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.ValidGreenPredicate
 
checkInvariants() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.TransformationData
 
checkRanges(ISSABasicBlock, ISSABasicBlock) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode
 
choiceGeneratorProcessed(VM, ChoiceGenerator<?>) - Method in class gov.nasa.jpf.symbc.VeritestingListener
 
choiceGeneratorRegistered(VM, ChoiceGenerator<?>, ThreadInfo, Instruction) - Method in class gov.nasa.jpf.symbc.VeritestingListener
 
ci - Variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
 
className - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef
 
ClassUtils - Class in gov.nasa.jpf.symbc.veritesting.VeritestingUtil
A utility class used during discovering of static regions.
ClassUtils() - Constructor for class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ClassUtils
 
cleanupTime - Static variable in class gov.nasa.jpf.symbc.VeritestingListener
 
clearStack(StackFrame, Instruction) - Static method in class gov.nasa.jpf.symbc.VeritestingListener
This pop up operands of the if instruction that begins the region.
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRef
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRefVarExpr
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.AstVarExpr
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.CloneableVariable
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRefVarExpr
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.def.WalaVarExpr
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayExpressions
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySubscriptMap
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.GlobalArraySubscriptMap
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FieldRefTypeTable
Clones the FieldRefTypeTable to a new FieldRefTypeTable, by creating new entries for the keys.
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.ValueSymbolTable
Clones the VarTypeTable to a new VarTypeTable, by creating new entries for the keys.
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSubscriptMap
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.GlobalSubscriptMap
 
clone() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubscriptPair
 
CloneableVariable - Class in gov.nasa.jpf.symbc.veritesting.ast.def
 
CloneableVariable(String) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.CloneableVariable
 
CloneableVarTable<T> - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment
Base class for all environment tables that use a Expression object as the key.
CloneableVarTable() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.CloneableVarTable
 
CloneableVarTable(String, String, String) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.CloneableVarTable
 
collect_constraints - Static variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
 
collectPredicates(ThreadInfo) - Static method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization
 
collectStaticAnalysisMetrics(HashMap<String, StaticRegion>) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager
 
collectTransformationState(FixedPointAstMapVisitor) - Static method in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper
sets if change has happened and also sets up the transformation responsible for the change;
combine - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor
 
combine - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor
 
compose(Stmt, Stmt, boolean) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil
 
CompositionStmt - Class in gov.nasa.jpf.symbc.veritesting.ast.def
RangerIR composition statement.
CompositionStmt(Stmt, Stmt) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.CompositionStmt
 
compositionStmt(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor
Transform a composition statement into a conjunction in green.
compositionStmt(CompositionStmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor
Transform a composition statement into a conjunction in green.
computeMethodInputVars(SlotParamTable) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.InputTable
This populates the InputTable for a methodRegion using the SlotParamTable since the InputTable for methodRegions is contains the same elements of the SlotParamTable.
computeMethodOutput(IR) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable
All normal predecessors of an exit node must have a return as the last instruction.
computeOutputVars(IR, SlotParamTable, InputTable, Pair<Integer, Integer>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable
outputVars are computed by finding the maximum wala var for each stackSlot and those that are not input or constants.
computeRegionBoundary(Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion
This computes the region boundary in case of conditional region, to determine the first use and the first and last def variables inside the region.
computeRegionInput(SlotParamTable, Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.InputTable
Computes inputs by visiting statement of the region and figuring out the first use of every stack slot that has no def as its first use.
concolicMode - Static variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory
 
concreteNumber - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionStatistics
counts the number of times we hit a region and it was concrete
condition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.GammaVarExpr
 
condition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseExpr
 
condition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseStmt
 
condition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FirstITEStmtVisitor
 
condition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns.ReturnResult
 
condition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiCondition
 
conditionalBranch(SSACFG, ISSABasicBlock, ISSABasicBlock) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
Attempts to translate a conditional part of the cfg to IfThenElse statement in RangerIR.
conditionList - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns
 
conjoin(Stmt, Stmt) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
This creates a composition statement between two statements
conjunct(List<Expression>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor
 
constantsTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor
 
constantsTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor
 
constantsTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion
 
constPropTime - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager
 
constructArrayITE(Expression, int, Pair<Expression[], String>) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayUtil
 
constructMethodIdentifier(String) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
Create the key of a Method region.
constructMethodIdentifier(ISSABasicBlock) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
 
constructRegionIdentifier(String, int) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
 
constructRegionIdentifier(IR, ISSABasicBlock) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
Create the key of a conditional region, by using the name as well as the bytecode offset of the last instruction in the first block that starts the region.
constructSortedBlockPQ() - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil
 
convert(SSAInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor
 
convert(SSAInstruction) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor
 
convertCondition(IR, SSAConditionalBranchInstruction) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil
 
convertOperator(IConditionalBranchInstruction.Operator) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil
 
convertToJavaName(String) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor
 
convertWalaVar(IR, int) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil
 
countException(Exception, StaticRegionException.ExceptionPhase) - Static method in exception gov.nasa.jpf.symbc.veritesting.StaticRegionException
 
create(DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor
 
create(ThreadInfo, DynamicRegion, int, boolean) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor
 
createArrayCondition(ArrayRefVarExpr) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor
 
createComplexIfCondition(ISSABasicBlock, ISSABasicBlock) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
Re-constructs a complex condition for an if/then/else condition.
createGamma(List<LinkedList<PhiCondition>>, List<Expression>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor
Creates Gamma Expression by visiting corresponding Phi
createGammaStmt(Expression, FieldRef, SubscriptPair, SubscriptPair) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor
 
createGammaStmtArray(int, Expression, Expression[], Expression[], String) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor
 
createGreenVar(String, String) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil
Creates a Green variable depending on its type.
createPC(PathCondition, Expression, Expression) - Static method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator
 
createSPFVariableForType(StackFrame, int, String) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil
This creates SPF constants depending on the type of the variable.
CreateStaticRegions - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst
This class creates our structure IR from the WALA SSA form, this is basically done by decompiling DAGs within a Java program.
CreateStaticRegions(IR, HashSet<NatLoop>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
 
createStructuredConditionalRegions(ISSABasicBlock, ISSABasicBlock, HashMap<String, StaticRegion>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
This class walks through method, attempting to find conditional veritesting regions
createStructuredConditionalRegions(HashMap<String, StaticRegion>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
 
createStructuredMethodRegion(HashMap<String, StaticRegion>) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
This class walks through method, attempting to find method regions veritesting regions
createSubscript(Integer) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.GlobalArraySubscriptMap
 
createSubscript(FieldRef) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor
 
createSubscript(FieldRef) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.GlobalSubscriptMap
 
currentBlock - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor
current block where the instruction lies.
currentClassName - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
 
currentCondition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor
 
currentCondition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor
Corresponds to the current condition during walking the CFG.
currentCondition - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
Keeps track of the current conditions/depth while visiting nodes in the graph.
currentMethodName - Variable in class gov.nasa.jpf.symbc.SymbolicListener
 
currentMethodName - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
 
currentPackageName - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain
 
currentTopFrame - Variable in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator
 
A B C D E F G H I J K L M N O P R S T U V W Z 
Skip navigation links