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 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

I2C - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

I2D - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

I2F - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

I2L - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

I2S - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IADD - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IALOAD - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IAND - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IArraySet - Interface in korat.finitization

Interface IArraySet represents field domain (set of values a field can take) for array fields.

IASTORE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IBitReader - Interface in korat.utils.io

Interface for reading bits (e.g. from InputStream, RandomFileAccess etc.)

IBitWriter - Interface in korat.utils.io

Interface for writing bits (e.g. to OutputStream, RandomFileAccess, etc.)

IBooleanSet - Interface in korat.finitization

IBooleanSet represents field domain for boolean fields

IByteSet - Interface in korat.finitization

IByteSet represents field domain for byte fields

IClassDomain - Interface in korat.finitization

Class domain is a set of objects of some concrete reference type.

IComparingFilter - Interface in korat.loading.filter

ICONST_0 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ICONST_1 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ICONST_2 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ICONST_3 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ICONST_4 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ICONST_5 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ICONST_M1 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ICVFactory - Interface in korat.utils.cv

ICVFinder - Interface in korat.utils.cv

Interface for searching for candidate vectors in the given candidate-vectors-file.

ICVReader - Interface in korat.utils.cv

Interface for sequential reading of candidate vectors from the candidate-vectors-file.

ICVWriter - Interface in korat.utils.cv

Interface for writing candidate vectors to a file.

ID_FIELD_PREFIX - Static variable in class korat.instrumentation.InstrumentationManager

IdentityWrapper - Class in korat.utils

IdentityWrapper(Object) - Constructor for class korat.utils.IdentityWrapper

IDeserializer - Interface in korat.utils.io

IDIV - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IDoubleSet - Interface in korat.finitization

IDoubleSet represents field domain for double fields

idx - Variable in class korat.gui.viz.VizListener

idx - Variable in class korat.instrumentation.bytecode.BytecodeInstruction

IF_ACMPEQ - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IF_ACMPNE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IF_ICMPEQ - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IF_ICMPGE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IF_ICMPGT - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IF_ICMPLE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IF_ICMPLT - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IF_ICMPNE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IFEQ - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IFGE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IFGT - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IFieldDomain - Interface in korat.finitization

Interface that represents Field domains.

IFilter - Interface in korat.loading.filter

IFinitization - Interface in korat.finitization

The IFinitization interface is used to set up the bounds for the search.

IFinitizationFactory - Interface in korat.finitization

ifInstr(CtClass) - Method in class korat.instrumentation.bytecode.StackTracerVisitor

Takes two values on top of the operand stack.

IFLE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IFloatSet - Interface in korat.finitization

Interface that represents field domain of the primitive type float.

IFLT - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IFNE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IFNONNULL - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IFNULL - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IINC - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IInstrumenter - Interface in korat.instrumentation

Base interface for instrumenter classes

IIntList - Interface in korat.utils

IIntSet - Interface in korat.finitization

Interface that represents field domain of the primitive type int.

IKoratArray - Interface in korat.instrumentation

IKoratArray represents korat arrays.

IKoratSearchStrategy - Interface in korat.testing

IKoratTouchable - Interface in korat.instrumentation

IKoratTouchable interface is applied to all instrumented classes.

ILLEGAL - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ILOAD - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ILOAD_0 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ILOAD_1 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ILOAD_2 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ILOAD_3 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ILongSet - Interface in korat.finitization

Interface that represents field domain of the primitive type long.

implementIKoratTouchableInterface(CtClass) - Method in class korat.instrumentation.ArrayGenerator

Implements IKoratTouchable interface by creating one field and two methods, specified by this interface //*actual field and method names may be different boolean koratTouched; public void __korat__touch__initialize() { if (!

IMUL - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

inBuff - Variable in class korat.utils.io.BitRandomAccessFile

inBuffSize - Variable in class korat.utils.io.BitRandomAccessFile

incCV(int[]) - Static method in class korat.utils.cv.CVSim

includedFinitizations - Variable in class korat.finitization.impl.Finitization

includeFinitization(IFinitization) - Method in interface korat.finitization.IFinitization

Includes information from finitization fin into current finitization.

includeFinitization(IFinitization) - Method in class korat.finitization.impl.Finitization

includeInIsomorphismCheck(boolean) - Method in interface korat.finitization.IClassDomain

If this option is set, the class domain will be included in isomorphism checking.

includeInIsomorphismCheck(boolean) - Method in class korat.finitization.impl.ClassDomain

IncludingPackageFilter - Class in korat.loading.filter

Confirms if some package is contained in list of packages

IncludingPackageFilter() - Constructor for class korat.loading.filter.IncludingPackageFilter

index - Variable in class korat.utils.cv.C.Pair

index - Variable in class korat.utils.cv.WriteCVListener.WriteNumMode

indexInStateSpace - Variable in class korat.finitization.impl.CVElem

indexOfFirstObjectInNextClassDomain - Variable in class korat.finitization.impl.ObjSet.CacheElement

indexType - Static variable in class korat.instrumentation.ArrayGenerator

INEG - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

init(int) - Method in class korat.utils.cv.WriteCVListener

init(int) - Method in class korat.utils.cv.WriteCVListenerSim

initAtomNames() - Method in class korat.gui.viz.metamodel.AtomFactory

initBuffer() - Method in class korat.utils.cv.CVFinderDelta

initCandArray(int) - Method in class korat.utils.cv.WriteCVListener.WriteNumExpectedMode

initCandArray(int) - Method in class korat.utils.cv.WriteCVListener.WriteNumMode

initCVWriter() - Method in class korat.utils.cv.WriteCVListener

initHandlePCs(MethodInfo) - Method in class korat.instrumentation.bytecode.StackTracerVisitor

initialize(int) - Method in class korat.finitization.impl.ArrayElementCVElem

initialize() - Method in class korat.finitization.impl.ClassDomain

Creates all uncreated objects.

initialize(int) - Method in class korat.finitization.impl.CVElem

Initializes this CVElem

initialize() - Method in class korat.finitization.impl.Finitization

Does all needed initialization.

initialize() - Method in class korat.finitization.impl.NullClassDomain

initialize() - Method in class korat.finitization.impl.StateSpace

Initializes the state space

initialize(ITester) - Method in interface korat.instrumentation.IKoratArray

Initializes array with ITester object to which the accessed field indexes will be reported

initialize() - Method in class korat.loading.InstrumentingClassLoader

initialize() - Method in class korat.utils.io.SimpleSerializer

initializeArray(IKoratArray, ITester) - Static method in class korat.instrumentation.KoratArrayManager

initializeClassDomains() - Method in class korat.finitization.impl.Finitization

initialized - Variable in class korat.finitization.impl.ClassDomain

initialized - Variable in class korat.finitization.impl.CVElem

initialized - Variable in class korat.finitization.impl.StateSpace

initializeFieldMap() - Method in class korat.finitization.impl.StateSpace

initializeFieldSetters() - Method in class korat.finitization.impl.Finitization

initKoratOptions() - Method in class korat.config.ConfigLoader

initialize koratOptions with all declared options

initLocals(CtClass, MethodInfo) - Method in class korat.instrumentation.bytecode.StackTracerVisitor

initMode(int) - Method in class korat.utils.cv.WriteCVListener

initSize - Variable in class korat.utils.IntList

initStartAndEndCVs(IKoratSearchStrategy) - Method in class korat.testing.impl.TestCradle

initStuffFromOptions() - Method in class korat.config.ConfigLoader

Initializes stuff from the previously parsed options.

instance - Static variable in class korat.config.ConfigManager

instance - Static variable in class korat.finitization.impl.FinitizationFactory

instance - Static variable in class korat.finitization.impl.NullClassDomain

instance - Static variable in class korat.gui.viz.metamodel.AtomFactory

instance - Static variable in class korat.gui.viz.metamodel.FieldFactory

instance - Static variable in class korat.gui.viz.metamodel.SigFactory

instance - Static variable in class korat.testing.impl.TestCradle

instance - Static variable in class korat.utils.BytecodeDumper

instance - Static variable in class korat.utils.cv.CVFactoryDelta

instanceFileNames - Variable in class korat.gui.viz.VizListener

INSTANCEOF - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

instrument(CtClass) - Method in class korat.instrumentation.AbstractInstrumenter

instrument(CtClass) - Method in class korat.instrumentation.CompoundInstrumenter

instrument(CtClass) - Method in class korat.instrumentation.FieldInstrumenter

instrument(CtClass) - Method in class korat.instrumentation.SpecialConstructorInstrumenter

instrument(CtClass) - Method in class korat.instrumentation.TouchInstrumenter

Deprecated.

InstrumentationManager - Class in korat.instrumentation

The place for various constants, utility method and such related to instrumentation.

InstrumentationManager() - Constructor for class korat.instrumentation.InstrumentationManager

instrumentClassIfNeeded(CtClass) - Static method in class korat.instrumentation.InstrumentationManager

Instruments the given class if not already instrumented

instrumenter - Static variable in class korat.instrumentation.InstrumentationManager

instrumenter - Variable in class korat.loading.InstrumentingClassLoader

instrumenters - Variable in class korat.instrumentation.CompoundInstrumenter

instrumentFieldDeclarations(CtClass) - Method in class korat.instrumentation.ArrayFieldInstrumenter

instrumentFieldDeclarations(CtClass) - Method in class korat.instrumentation.FieldInstrumenter

For each field in the given class adds additional stuff needed for instrumentation (by calling handleFieldDeclaration.

InstrumentingClassLoader - Class in korat.loading

InstrumentingClassLoader() - Constructor for class korat.loading.InstrumentingClassLoader

INT2BYTE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

INT2CHAR - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

INT2SHORT - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

interrupt() - Method in class korat.testing.impl.AbstractTestCaseGenerator

interrupted - Variable in class korat.testing.impl.AbstractTestCaseGenerator

IntList - Class in korat.utils

Slow - use one of its derivatives, BS or AI

IntList() - Constructor for class korat.utils.IntList

IntListAI - Class in korat.utils

List of integers with stack policy Different mechanism for checking if the field index is already contained in the accessed field list.

IntListAI(int) - Constructor for class korat.utils.IntListAI

IntListBS - Class in korat.utils

Uses bitset to check if field is already contained.

IntListBS() - Constructor for class korat.utils.IntListBS

IntListBS(int) - Constructor for class korat.utils.IntListBS

IntSet - Class in korat.finitization.impl

IntSet(int, int, int) - Constructor for class korat.finitization.impl.IntSet

IntSet(int, int) - Constructor for class korat.finitization.impl.IntSet

IntSet(int) - Constructor for class korat.finitization.impl.IntSet

intType - Variable in class korat.instrumentation.bytecode.JavassistInstructionVisitor

invoke(Object, String, Class[], Object[]) - Static method in class korat.utils.ReflectionUtils

Invokes method of a given obj and set of parameters

invokeFinMethod(Class, Method, String[]) - Method in class korat.testing.impl.TestCradle

invokeInstr(boolean, boolean, int) - Method in class korat.instrumentation.bytecode.StackTracerVisitor

Pops the right number of values from the top of the operand stack (which is equal to the number of method parameters of the method to be invoked), then if the call is not static pops object reference from the operand stack, and finally pushes the return type of the method to the stack.

INVOKEINTERFACE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

INVOKENONVIRTUAL - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

INVOKESPECIAL - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

INVOKESTATIC - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

INVOKEVIRTUAL - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IObjSet - Interface in korat.finitization

Interface that represents Field domains for reference types.

IOR - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IPrimitiveTypeSet - Interface in korat.finitization

Interface that represents Field domain for primitive type.

IREM - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IRETURN - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

isArrayStore() - Method in class korat.instrumentation.bytecode.BytecodeInstruction

isArrayType() - Method in interface korat.finitization.IFieldDomain

Does this field domain represent array type.

isArrayType() - Method in class korat.finitization.impl.ArraySet

isArrayType() - Method in class korat.finitization.impl.BooleanSet

isArrayType() - Method in class korat.finitization.impl.ObjSet

isArrayType() - Method in class korat.finitization.impl.PrimitiveTypeSet

isCacheValid - Variable in class korat.finitization.impl.ObjSet

isEmpty() - Method in class korat.instrumentation.bytecode.OperandStack

isEmpty() - Method in interface korat.utils.IIntList

Returns true if there are no elements in the list, false if there is at least one element in the list

isEmpty() - Method in class korat.utils.IntList

isEmpty() - Method in class korat.utils.IntListAI

ISerializer - Interface in korat.utils.io

isExcludedFromSearch() - Method in class korat.finitization.impl.CVElem

ISHL - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IShortSet - Interface in korat.finitization

Interface that represents field domain of the primitive type short.

ISHR - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

isIncludedInIsomorphismChecking() - Method in interface korat.finitization.IClassDomain

isIncludedInIsomorphismChecking() - Method in class korat.finitization.impl.ClassDomain

isInitialized() - Method in class korat.finitization.impl.ClassDomain

isInterrupted() - Method in class korat.testing.impl.AbstractTestCaseGenerator

isInvoke() - Method in class korat.instrumentation.bytecode.BytecodeInstruction

isKoratField(String) - Static method in class korat.instrumentation.InstrumentationManager

isKoratMethod(String) - Static method in class korat.instrumentation.InstrumentationManager

isLocalStore() - Method in class korat.instrumentation.bytecode.BytecodeInstruction

isNullAllowed() - Method in class korat.finitization.impl.ObjSet

isNullAllowed() - Method in interface korat.finitization.IObjSet

Is null allowed or not.

isomorphismCheck - Variable in class korat.finitization.impl.ClassDomain

isPredicateOK() - Method in class korat.testing.impl.TestCradle

isPredicateOK() - Method in class korat.utils.cv.CVFinder

isPredicateOK() - Method in class korat.utils.cv.CVFinderDelta

isPredicateOK() - Method in class korat.utils.cv.CVReader

isPredicateOK() - Method in class korat.utils.cv.CVReaderDelta

isPredicateOK() - Method in interface korat.utils.cv.ICVFinder

Call this method immediately after calling readCV to find out if the read vector passes predicate check or not

isPredicateOK() - Method in interface korat.utils.cv.ICVReader

Call this method immediately after calling readCV to find out if the read vector passes predicate check or not

isPrimitive() - Method in class korat.gui.viz.metamodel.AlloySig

isPrimitiveType() - Method in interface korat.finitization.IFieldDomain

Does this field domain represent primitive type.

isPrimitiveType() - Method in class korat.finitization.impl.ArraySet

isPrimitiveType() - Method in class korat.finitization.impl.BooleanSet

isPrimitiveType() - Method in class korat.finitization.impl.ObjSet

isPrimitiveType() - Method in class korat.finitization.impl.PrimitiveTypeSet

isPutField() - Method in class korat.instrumentation.bytecode.BytecodeInstruction

ISTORE - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ISTORE_0 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ISTORE_1 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ISTORE_2 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ISTORE_3 - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ISUB - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

ITestCaseListener - Interface in korat.testing

Client that should handle test structures

ITester - Interface in korat.testing

Interface for a class that should communicate with the debugger

ITransformingFilter<Type> - Interface in korat.loading.filter

Base interface for all filters that transform input

IUSHR - Static variable in class korat.instrumentation.bytecode.BytecodeUtils

IXOR - Static variable in class korat.instrumentation.bytecode.BytecodeUtils