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

A

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

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

AbstractInstrumenter - Class in korat.instrumentation

Base instrumenter class.

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

AbstractTestCaseGenerator - Class in korat.testing.impl

AbstractTestCaseGenerator() - Constructor for class korat.testing.impl.AbstractTestCaseGenerator

AbstractTestCaseGenerator(PrintStream) - Constructor for class korat.testing.impl.AbstractTestCaseGenerator

accept(BytecodeVisitor) - Method in class korat.instrumentation.bytecode.BytecodeInstruction

accessedFields - Variable in class korat.testing.impl.StateSpaceExplorer

accessedFields - Variable in class korat.testing.impl.TestCradle

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

add(AbstractInstrumenter) - Method in class korat.instrumentation.CompoundInstrumenter

add(IComparingFilter) - Method in class korat.loading.filter.CompoundComparingFilter

add(IComparingFilter[]) - Method in class korat.loading.filter.CompoundComparingFilter

add(Object[]) - Method in class korat.loading.filter.CompoundComparingFilter

add(int) - Method in interface korat.utils.IIntList

Adds an element to the end of IIntList.

add(int) - Method in class korat.utils.IntList

add(int) - Method in class korat.utils.IntListAI

add(int) - Method in class korat.utils.IntListBS

addAll(String, IObjSet) - Method in interface korat.finitization.IFinitization

Adds all objects from the given objSet to the given field which has to be of type Collection.

addAll(String, String, IObjSet) - Method in interface korat.finitization.IFinitization

Adds all objects from the given objSet to the given field which has to be of type Collection.

addAll(Class, String, IObjSet) - Method in interface korat.finitization.IFinitization

Adds all objects from the given objSet to the given field which has to be of type Collection.

addAll(String, IObjSet) - Method in class korat.finitization.impl.Finitization

addAll(String, String, IObjSet) - Method in class korat.finitization.impl.Finitization

addAll(Class, String, IObjSet) - Method in class korat.finitization.impl.Finitization

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

addByte(byte) - Method in interface korat.finitization.IByteSet

addByte(byte) - Method in class korat.finitization.impl.ByteSet

addClassDomain(IClassDomain) - Method in class korat.finitization.impl.ObjSet

addClassDomain(IClassDomain) - Method in interface korat.finitization.IObjSet

Adds new class domain.

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

Adds needed constructors to class under test First, if doesn't exist, no-arg constructor is added with empty body.

addDouble(double) - Method in interface korat.finitization.IDoubleSet

addDouble(double) - Method in class korat.finitization.impl.DoubleSet

addFilter(IComparingFilter) - Static method in class korat.loading.filter.FilterManager

addFloat(float) - Method in interface korat.finitization.IFloatSet

addFloat(float) - Method in class korat.finitization.impl.FloatSet

addGetSetterMethod(CtClass, CtField) - Method in class korat.instrumentation.FieldInstrumenter

Adds getter method for the setter of the given field.

addGetterMethod(CtClass, CtField) - Method in class korat.instrumentation.FieldInstrumenter

Adds special getter method which before returning the value of the field notifies the instance of the ITestCradle about the field access.

addIdField(CtClass, CtField) - Method in class korat.instrumentation.FieldInstrumenter

Just adds one extra int field.

addInt(int) - Method in interface korat.finitization.IIntSet

addInt(int) - Method in class korat.finitization.impl.IntSet

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

Adds ITester field that holds an instance of the ITester class that should be notified about field accesses.

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

Adds a special constructor that Korat will call to initialize object under test.

addLong(long) - Method in interface korat.finitization.ILongSet

addLong(long) - Method in class korat.finitization.impl.LongSet

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

Adds no-arg constructor with empty body.

addObject(Object) - Method in interface korat.finitization.IClassDomain

Add existing object into class domain.

addObject(Object) - Method in class korat.finitization.impl.ClassDomain

addObjects(Object[]) - Method in interface korat.finitization.IClassDomain

Add all objects of the existing array to the class domain

addObjects(Collection) - Method in interface korat.finitization.IClassDomain

Add all objects of the existing collection to the class domain

addObjects(Object[]) - Method in class korat.finitization.impl.ClassDomain

addObjects(Collection) - Method in class korat.finitization.impl.ClassDomain

addPackage(String) - Method in class korat.loading.filter.PackageFilter

addRange(byte, byte, byte) - Method in interface korat.finitization.IByteSet

addRange(double, double, double) - Method in interface korat.finitization.IDoubleSet

addRange(float, float, float) - Method in interface korat.finitization.IFloatSet

addRange(int, int, int) - Method in interface korat.finitization.IIntSet

addRange(long, long, long) - Method in interface korat.finitization.ILongSet

addRange(byte, byte, byte) - Method in class korat.finitization.impl.ByteSet

addRange(double, double, double) - Method in class korat.finitization.impl.DoubleSet

addRange(float, float, float) - Method in class korat.finitization.impl.FloatSet

addRange(int, int, int) - Method in class korat.finitization.impl.IntSet

addRange(long, long, long) - Method in class korat.finitization.impl.LongSet

addRange(short, short, short) - Method in class korat.finitization.impl.ShortSet

addRange(short, short, short) - Method in interface korat.finitization.IShortSet

addShort(short) - Method in class korat.finitization.impl.ShortSet

addShort(short) - Method in interface korat.finitization.IShortSet

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

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

Deprecated. Implements KoratTouchable interface

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

Deprecated.

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

Deprecated. Initializes process of touching by resetting __korat__touched flag.

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

Deprecated. Adds touch method to the class that accesses all fields of given object and invokes touch method on all objects associated with accessed fields.

addTrace(String) - Method in class korat.instrumentation.ArrayGenerator

Used to show debug messages inside the generated classes This instrumentation is applied only if trace flag is set.

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

Deprecated. Adds __korat__touched boolean flag, which signals whether this object has already been touched.

AlgSimulator - Class in korat.utils.cv

Simulates algorithm that saves equidistant vectors

AlgSimulator() - Constructor for class korat.utils.cv.AlgSimulator

allAtoms - Variable in class korat.gui.viz.metamodel.AtomFactory

allAtomsOrdered - Variable in class korat.gui.viz.metamodel.AtomFactory

allFields - Variable in class korat.gui.viz.metamodel.FieldFactory

allowProcessing(String) - Method in class korat.loading.filter.CompoundComparingFilter

allowProcessing(String) - Method in class korat.loading.filter.DefaultFilters.ExcludeKoratPackagesFilter

allowProcessing(String) - Method in class korat.loading.filter.DefaultFilters.ExcludeSystemPackagesFilter

allowProcessing(String) - Method in class korat.loading.filter.ExcludingPackageFilter

Returns true if package of className class in not the one in the list of excluded packages

allowProcessing(String) - Method in interface korat.loading.filter.IComparingFilter

allowProcessing(String) - Method in class korat.loading.filter.IncludingPackageFilter

AlloyAtom - Class in korat.gui.viz.metamodel

AlloyAtom(AlloySig, String, Object) - Constructor for class korat.gui.viz.metamodel.AlloyAtom

AlloyField - Class in korat.gui.viz.metamodel

Use FieldFactory to create object of this type.

AlloyField(String) - Constructor for class korat.gui.viz.metamodel.AlloyField

AlloySig - Class in korat.gui.viz.metamodel

Use SigFactory to create object of this type.

AlloySig(String) - Constructor for class korat.gui.viz.metamodel.AlloySig

AlloySig(String, AlloySig) - Constructor for class korat.gui.viz.metamodel.AlloySig

allSigs - Variable in class korat.gui.viz.metamodel.SigFactory

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

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

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

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

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

alreadyInstrumented - Static variable in class korat.instrumentation.InstrumentationManager

global repository of the instrumented classes

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

appendClassDomain(List<CVElem>, ClassDomain) - Method in class korat.finitization.impl.Finitization

appendFields(List<CVElem>, Object, Map<String, IFieldDomain>) - Method in class korat.finitization.impl.Finitization

appendSuffix(File, int) - Static method in class korat.utils.io.FileUtils

appends special suffix (number of all files) to all files within given directory

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

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

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

argDefValue - Variable in class korat.config.MyOption

ARGS - Static variable in class korat.config.ConfigLoader

args - Variable in class korat.config.ConfigManager

Array of arguments to be passed to the finitization method.

ARRAY_FULLNAME_PREFIX - Static variable in class korat.instrumentation.ArrayGenerator

ArrayBytecodesVisitor - Class in korat.instrumentation.bytecode

Visitor that handles each bytecode instruction in order to instrument all accesses to array fields.

ArrayBytecodesVisitor(ClassPool, ConstPool, OperandStack) - Constructor for class korat.instrumentation.bytecode.ArrayBytecodesVisitor

ArrayElementCVElem - Class in korat.finitization.impl

CVElem representing elements of an array

ArrayElementCVElem(Object, int, FieldDomain, StateSpace) - Constructor for class korat.finitization.impl.ArrayElementCVElem

ArrayElementCVElem(Object, String, FieldDomain, StateSpace) - Constructor for class korat.finitization.impl.ArrayElementCVElem

ArrayFieldInstrumenter - Class in korat.instrumentation

This class does all the instrumentation related to array fields.

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

ArrayGenerator - Class in korat.instrumentation

ArrayGenerator is used to generate Korat Array classes.

ArrayGenerator(CtClass) - Constructor for class korat.instrumentation.ArrayGenerator

Creates korat array for the given type of array, which is represented as javassist CtClass.

ArrayGenerator(Class) - Constructor for class korat.instrumentation.ArrayGenerator

arrayIndex - Variable in class korat.finitization.impl.ArrayElementCVElem

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

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

Pops index and array values from the operand stack and pushes the array's component type which is provided through the type parameter.

arrayPushed - Variable in class korat.instrumentation.bytecode.StackTracerVisitor

arrays - Variable in class korat.finitization.impl.ArraySet

ArraySet - Class in korat.finitization.impl

ArraySet(ClassDomain, IntSet, FieldDomain) - Constructor for class korat.finitization.impl.ArraySet

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

Pops value, index and array values from the operand stack.

arrayType - Variable in class korat.instrumentation.ArrayGenerator

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

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

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

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

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

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

AtomFactory - Class in korat.gui.viz.metamodel

AtomFactory() - Constructor for class korat.gui.viz.metamodel.AtomFactory

atoms - Variable in class korat.gui.viz.metamodel.AlloySig

attachClient(ITestCaseListener) - Method in class korat.testing.impl.AbstractTestCaseGenerator

attachSpecialClient(ITestCaseListener) - Method in class korat.testing.impl.AbstractTestCaseGenerator