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