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

D

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

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

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

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

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

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

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

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

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

debugMode - Static variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

declaredResultTypes - Variable in class gov.nasa.jpf.symbc.veritesting.ast.def.CheckCastInstruction

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

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

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

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

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

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

DefaultTransformation - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations

Abstract class that defines transformation execution and then checking its invariants.

DefaultTransformation() - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.DefaultTransformation

defaultVal - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor

defaultVal - Variable in class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor

defUseVisit - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor

DefUseVisit - Enum in gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst

Enum that carries two values, either a def or a use.

DefUseVisit() - Constructor for enum gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.DefUseVisit

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

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

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

discoverAllClassAndGetRegion(String, String, String) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.JITAnalysis

discoverRegions(ThreadInfo, Instruction, String) - Static method in class gov.nasa.jpf.symbc.veritesting.VeritestingUtil.JITAnalysis

This is tries to discover statically all potential regions that could be used as veritesting regions.

discoverRegions(ThreadInfo) - Method in class gov.nasa.jpf.symbc.VeritestingListener

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

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

doArrayStore(ThreadInfo, ArrayExpressions, DynamicTable<Expression>) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayUtil

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

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

doTransform(ThreadInfo, DynamicRegion) - Static method in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldAccessVisitor

dp - Static variable in class gov.nasa.jpf.symbc.SymbolicInstructionFactory

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

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

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

DynamicOutputTable(String, String, String) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicOutputTable

DynamicOutputTable(OutputTable, int) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicOutputTable

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

This class represents a DynamicRegion, that is, a StaticRegion that has been processed dynamically, this is done initially through uniquness transformation then later with the substitution and other transformations.

DynamicRegion(DynamicRegion, Stmt, SPFCaseList, Expression, Expression, RemoveEarlyReturns.ReturnResult) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion

DynamicRegion(StaticRegion, Stmt, int, RemoveEarlyReturns.ReturnResult) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion

Constructor that is used to create a dynamic region out of a static region.

DynamicTable<V> - Class in gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment

DynamicTable(String, String, String) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicTable

DynamicTable(String, String, String, ArrayList<Variable>, ArrayList<V>) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicTable

DynamicTable(StaticTable, int) - Constructor for class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicTable

dynRegion - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor

dynRegion - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor

dynRegion - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor

dynRegion - Variable in class gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor

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

dynRegion - Static variable in class gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

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

A statement that represents the region after instantiation.

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