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

I

i2b() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

i2c() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

i2d() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

i2f() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

i2l() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

i2s() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

iadd() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

iaload() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

iand() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

iastore() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

idiv() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

if_icmpeq(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

if_icmpge(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

if_icmpgt(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

if_icmple(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

if_icmplt(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

if_icmpne(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ifCondCache - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor

ifeq(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ifge(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ifgt(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ifle(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

iflt(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ifne(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ifnonnull(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ifnull(int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ifRemovedCount - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

IfThenElseExpr - Class in gov.nasa.jpf.symbc.veritesting.ast.def

This is IfThenElse expression in Ranger IR

IfThenElseExpr(Expression, Expression, Expression) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseExpr

IfThenElseStmt - Class in gov.nasa.jpf.symbc.veritesting.ast.def

This is the IfThenElseStmt in RangerIR that carries a condition instruction and on the "then" and the "else" side the statements extracted from the cfg that represents the two sides of the branch.

IfThenElseStmt(SSAConditionalBranchInstruction, Expression, Stmt, Stmt) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseStmt

iinc(int, int) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

imul() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

incrementFailure(Expression) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.ValidGreenPredicate

incrementPathCount() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionHitExactHeuristic

incrementRegionExactHeuristicCount(Instruction) - Static method in class gov.nasa.jpf.symbc.veritesting.Heuristics.HeuristicManager

ind() - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

indent - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

indent() - Method in class gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor

index - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLoadInstruction

index - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRef

index - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.ArrayStoreInstruction

ineg() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

inializeQueriesFile - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

initializeTime - Static variable in class gov.nasa.jpf.symbc.VeritestingListener

inputTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion

A table that holds inputs to the region.

InputTable - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment

This class populates the input variables for the region, it does so by computing the first var use for every slot in case of non-method region, or computing the parameters of a method as the input table in case of a method region.

InputTable(IR, boolean, SlotParamTable, Stmt) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.InputTable

InputTable(boolean, IR) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.InputTable

inputTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprRegionInputVisitor

inputTable - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion

An environment table that defines the input vars to the region.

InstanceOfInstruction - Class in gov.nasa.jpf.symbc.veritesting.ast.def

This is InstanceOfInstruction in RangerIR that matches the corresponding InstanceOfInstruction in Wala and subsequently the instruction in Java Bytecode.

InstanceOfInstruction(SSAInstanceofInstruction, Expression, Expression, TypeReference) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.InstanceOfInstruction

InstanceOfInstruction(SSAInstanceofInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.InstanceOfInstruction

instantiatedRegion - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor

instantiationLimit - Static variable in class gov.nasa.jpf.symbc.VeritestingListener

instPhaseEx - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

Instruction - Class in gov.nasa.jpf.symbc.veritesting.ast.def

Abstract class that represents all instructions.

Instruction(SSAInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.Instruction

instruction - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.JITAnalysis

instructionExecuted(VM, ThreadInfo, Instruction, Instruction) - Method in class gov.nasa.jpf.symbc.SymbolicListener

instructionToExec - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

interestingClassNames - Static variable in class gov.nasa.jpf.symbc.VeritestingListener

interestingRegionCount - Static variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

Invariant - Interface in gov.nasa.jpf.symbc.veritesting.ast.transformations

An interface for checking invariants of every transformation.

invariants - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.TransformationData

invocationStack - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

invoke() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput

InvokeInstruction - Class in gov.nasa.jpf.symbc.veritesting.ast.def

This is InvokeInstruction in RangerIR that matches the corresponding InvokeInstruction in Wala and subsequently the corresponding instructions in Java Bytecode.

InvokeInstruction(SSAInvokeInstruction, Expression[], Expression[]) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.InvokeInstruction

InvokeInstruction(SSAInvokeInstruction) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.def.InvokeInstruction

invokeinterface(String, String, String) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

invokespecial(String, String, String) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

invokestatic(String, String, String) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

invokevirtual(String, String, String) - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ior() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ir - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion

This holds the static version of the region that is matching this instantiation.

ir - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.InputTable

ir - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

ir - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor

ir - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor

IR of the region currently being translated to RangerIR Statement.

ir - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor

ir - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor

ir - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions

ir - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion

IR of the method that the StaticRegion belongs to.

ir - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingMain

irem() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

isAllowedRecursiveCall(MethodReference) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

isAllowedRegion(String) - Method in class gov.nasa.jpf.symbc.VeritestingListener

isBothSidesFeasible(ThreadInfo, Comparator, Comparator, Expression, Expression) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil

isBranch(SSACFG, ISSABasicBlock) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions

isChangedFlag() - Static method in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

Returns if change has happened

isConditionalBranch(ISSABasicBlock) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil

isConstant(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

Determines if a wala var is constant.

isConstant(Expression) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.ExprTypeVisitor

isConstant(Expression) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil

isEqualRegion() - Static method in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

isFoundWalaVarExpr() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

ishl() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ishr() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

isIncrementalSolver() - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil

isInterestingRegion(String) - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

isLoopStart(HashSet<NatLoop>, ISSABasicBlock) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil

isMethodRegion - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion

Identifies if the dynamic region corresponds to a region that starts with a condition, or is it enclosing the summary of the whole method.

isMethodRegion - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.InputTable

isMethodRegion - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

isMethodRegion - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion

A boolean that indicates whether this is a conditional region,i.e, a region that begins with an if instruction, or a method region, i.e., a region that is summarizing the whole method.

isNoVeritesting(StackFrame, boolean) - Method in class gov.nasa.jpf.symbc.VeritestingListener

isNull() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns.ReturnResult

isOnlyStaticChoiceSat(DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator

isOutputVar(int) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable

isPCSat(PathCondition) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil

isRead - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput

isRecursiveCall(MethodReference) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor

isRegionEndOk(ThreadInfo, StaticRegion, Instruction) - Method in class gov.nasa.jpf.symbc.VeritestingListener

isSatGreenExpression(Expression) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil

isSatisfiable(PathCondition) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil

isSelfContainedSubgraph(ISSABasicBlock, ISSABasicBlock) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions

This method checks to see whether each node in a subgraph up to a terminus has a subgraph.

isSomethingChanged() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor

isStackConsumingRegionEnd(ThreadInfo, StaticRegion, Instruction) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil

isStatic - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef

isSymCond(ThreadInfo, Instruction) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil

Checks if the "if" condition is symbolic based on the the operands of the "if" bytecode instruction.

isSymCond(ThreadInfo, Stmt, SlotParamTable, Instruction) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil

Checks if the "if" condition is symbolic by visiting the condition expression of the statement of the staticRegion

isSymCondition - Variable in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

isSymCondition() - Method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor

isTrue() - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns.ReturnResult

isub() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

isUnsupportedArrayRef(ArrayRef) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

isVariable(Expression) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil

ite(Expression, Expression, Expression) - Method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

Translates conditional expression to a corresponding Green expression.

iterationNumber - Static variable in class gov.nasa.jpf.symbc.veritesting.FixedPointWrapper

iushr() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

ixor() - Method in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

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