Modifier and Type | Class and Description |
---|---|
class |
$coreTag
if this class can be loaded, the JPF core is in the CLASSPATH.
|
class |
AnnotationProxyBase
common stuff used by all Annotation Proxies
|
class |
BoxObjectCaches |
class |
CachedROHttpConnection
this is just a very rough abstraction at this point, which only supports
reading static URL contents.
|
class |
Config
class that encapsulates property-based JPF configuration.
|
class |
ConsoleOutputStream
this is what we use for System.out and System.err, hence we go native
as quickly as possible, hence we don't need an underlying stream.
|
class |
Error
class used to store property violations (property and path)
|
class |
GenericProperty
generic abstract base class implementing program properties.
|
class |
JPF
main class of the JPF verification framework.
|
static class |
JPF.ExitException
private helper class for local termination of JPF (without killing the
whole Java process via System.exit).
|
class |
JPFClassLoader
classloader that is used by Config to instantiate from JPF configured
paths.
|
class |
JPFConfigException
this class wraps the various exceptions we might encounter during
initialization and use of Config
|
class |
JPFErrorException
internal JPF error
|
class |
JPFException
common root for all exceptions thrown by JPF
|
class |
JPFListenerException
JPFException that wraps whatever can go wrong in a listener during notification
|
class |
JPFNativePeerException
JPFException that wraps whatever can go wrong in a native method
|
class |
ListenerAdapter
Adapter class that dummy implements both VMListener and SearchListener interfaces
Used to ease implementation of listeners that only process a few notifications
|
class |
PropertyListenerAdapter
abstract base class that dummy implements Property, Search- and VMListener methods
convenient for creating listeners that act as properties, just having to override
the methods they need
the only local functionality is that instances register themselves automatically
as property when the search is started
<2do> rewrite once GenericProperty is an interface
|
class |
SerializationConstructor<T> |
class |
State
abstraction of JPF execution state that can be queried and stored by
listeners
|
Modifier and Type | Field and Description |
---|---|
Object[] |
Config.CONFIG_ARGS |
static Object[] |
Config.NO_ARGS |
Modifier and Type | Method and Description |
---|---|
<T> T[] |
Config.getGroupInstances(String keyPrefix,
String keyPostfix,
Class<T> type,
String... defaultClsNames)
this one is used to instantiate objects from a list of keys that share
the same prefix, e.g.
|
Object |
Config.put(Object keyObject,
Object valueObject) |
Object |
Config.setProperty(String key,
String newValue) |
Modifier and Type | Method and Description |
---|---|
TreeMap<Object,Object> |
Config.asOrderedMap() |
TreeMap<Object,Object> |
Config.asOrderedMap() |
List<Object> |
Config.getSources() |
Modifier and Type | Method and Description |
---|---|
PrintStream |
ConsoleOutputStream.format(String fmt,
Object... args) |
<T> T |
Config.getEssentialInstance(String key,
Class<T> type,
Class<?>[] argTypes,
Object[] args) |
<T> T |
Config.getEssentialInstance(String key,
Class<T> type,
Object arg1,
Object arg2)
just a convenience method for ctor calls that take two arguments
|
<T> T |
Config.getInstance(String key,
Class<T> type,
Class<?>[] argTypes,
Object[] args) |
<T> T |
Config.getInstance(String key,
Class<T> type,
Object arg1,
Object arg2) |
<T> T |
Config.getInstance(String id,
String clsName,
Class<T> type,
Class<?>[] argTypes,
Object[] args) |
<T> ArrayList<T> |
Config.getInstances(String key,
Class<T> type,
Class<?>[] argTypes,
Object[] args) |
String |
Config.getSourceName(Object src) |
T |
SerializationConstructor.newInstance(Object... args) |
void |
ConsoleOutputStream.print(Object o) |
PrintStream |
ConsoleOutputStream.printf(String fmt,
Object... args) |
void |
ConsoleOutputStream.println(Object o) |
Object |
Config.put(Object keyObject,
Object valueObject) |
Modifier and Type | Class and Description |
---|---|
class |
ClassFile
class to read and dissect Java classfile contents (as specified by the Java VM
spec http://java.sun.com/docs/books/jvms/second_edition/html/ClassFile.doc.html#16628
|
class |
ClassFileParser
a class parser that reads Java class file formats
This is actually more of an adapter between the Java specific ClassFile (which does the real parsing),
and the Java agnostic ClassInfo, which is only accessed through its initialization API since it resides
in another package
|
class |
ClassFilePrinter
simple tool to print contents of a classfile
<2do> use indentation level variable and formated output
|
class |
ClassFileReaderAdapter
adapter class implementing the ClassFileReader interface
|
class |
DefaultJVMClassFactory
default implementation of a JVM specific ClassFactory
|
class |
DirClassFileContainer |
class |
JarClassFileContainer
a ClassFileContainer that loads classes from jar files
|
class |
JVMAnnotationParser
parser that reads annotation classfiles and extracts default value entries
Java annotations form a different type system.
|
class |
JVMByteCodePrinter
utility class that prints out bytecode in readable form
|
class |
JVMByteCodeReaderAdapter
empty implementation of a JVMByteCodeReader, to efficiently allow overriding
single methods
|
class |
JVMClassFileContainer
ClassFileContainer that holds Java classfiles
|
class |
JVMClassInfo
a ClassInfo that was created from a Java classfile
|
class |
JVMCodeBuilder
a special JVMByteCodeReader implementation that builds code arrays for
MethodInfos, setting index and pc on the fly
|
class |
JVMDirectCallStackFrame
a direct call stackframe that supports JVM calling conventions
|
class |
JVMInstruction
an Instruction class that implements an InstructionVisitorAcceptor
This is the common root class for all Java bytecodes
|
class |
JVMInstructionFactory
interface for bytecode creation
this deliberately uses the abstract abstract public Instruction as return type to allow different instruction hierarchies in
extensions.
|
class |
JVMNativeStackFrame
a NativeStackFrame used for calling NativeMethods from Java bytecode
|
class |
JVMStackFrame
a stackframe that is used for executing Java bytecode, supporting both
locals and an operand stack.
|
Modifier and Type | Method and Description |
---|---|
Object |
ClassFile.getConstValueAttribute(int dataPos) |
Object |
ClassFile.getCpValue(int i) |
Object |
JVMStackFrame.getLongResultAttr() |
Object |
JVMDirectCallStackFrame.getLongResultAttr() |
Object |
JVMStackFrame.getResultAttr() |
Object |
JVMDirectCallStackFrame.getResultAttr() |
Modifier and Type | Method and Description |
---|---|
void |
ClassFile.parseAnnotationDefaultAttr(ClassFileReader reader,
Object tag)
AnnotationDefault_attribute {
u2 attribute_name_index;
u4 attribute_length;
element_value default_value; << pos
}
|
void |
ClassFile.parseAnnotationsAttr(ClassFileReader reader,
Object tag) |
void |
ClassFile.parseBytecode(JVMByteCodeReader reader,
Object tag,
int codeLength) |
void |
ClassFile.parseCodeAttr(ClassFileReader reader,
Object tag)
(optionally) called by reader from within the setMethodAttribute() notification
This means we have recursive notification since this is a variable length
attribute that has variable length attributes
Code_attribute { u2 attr_name_index
|
protected void |
ClassFile.parseCodeAttrAttributes(ClassFileReader reader,
Object tag,
int attrCount) |
void |
ClassFile.parseConstValueAttr(ClassFileReader reader,
Object tag)
optionally called by reader to obtain a ConstantValue field attribute
ConstantValue {u2 attrName
|
void |
ClassFile.parseEnclosingMethodAttr(ClassFileReader reader,
Object tag)
EnclosingMethod_attribute {
u2 attribute_name_index;
u4 attribute_length;
u2 class_index -> Class_info { u1 tag; u2 name_index->utf8 }
u2 method_index -> NameAndType_info { u1 tag; u2 name_index->utf8; u2 descriptor_index->utf8 }
}
|
void |
ClassFile.parseExceptionAttr(ClassFileReader reader,
Object tag) |
void |
ClassFile.parseInnerClassesAttr(ClassFileReader reader,
Object tag)
(optionally) called by ClassFileReader from within setClassAttribute() notification
InnerClass { u2 nameIdx
|
void |
ClassFile.parseLineNumberTableAttr(ClassFileReader reader,
Object tag)
optionally called from ClassFileReader.setCodeAttribute() to parse LineNumberTables
LineNumberTable { u2 attrName; u4 attrLength;
u2 lineCount;
{ u2 startPc; u2 lineNumber; } [lineCount] };
pos is at lineCount
|
void |
ClassFile.parseLocalVarTableAttr(ClassFileReader reader,
Object tag)
optionally called from ClassFileReader.setCodeAttribute() to parse LocalVarTables
LocalVarTableTable { u2 attrName; u4 attrLength;
u2 localVarCount;
{ u2 startPc; u2 lineNumber; } [lineCount] };
pos is at localVarCount
|
void |
ClassFile.parseParameterAnnotationsAttr(ClassFileReader reader,
Object tag) |
void |
ClassFile.parseSignatureAttr(ClassFileReader reader,
Object tag)
Signature_attribute {
u2 attribute_name_index;
u4 attr-length;
u2 signature-index << pos
}
|
void |
ClassFile.parseSourceFileAttr(ClassFileReader reader,
Object tag)
(optionally) called by ClassFileReader from within setClassAttribute() notification
InnerClass { u2 nameIdx
|
void |
JVMAnnotationParser.setAnnotation(ClassFile cf,
Object tag,
int annotationIndex,
String annotationType) |
void |
ClassFileParser.setAnnotation(ClassFile cf,
Object tag,
int annotationIndex,
String annotationType) |
void |
ClassFilePrinter.setAnnotation(ClassFile cf,
Object tag,
int annotationIndex,
String annotationType) |
void |
ClassFileReaderAdapter.setAnnotation(ClassFile cf,
Object tag,
int annotationIndex,
String annotationType) |
void |
ClassFileReader.setAnnotation(ClassFile cf,
Object tag,
int annotationIndex,
String annotationType) |
void |
ClassFileParser.setAnnotationCount(ClassFile cf,
Object tag,
int annotationCount) |
void |
ClassFilePrinter.setAnnotationCount(ClassFile cf,
Object tag,
int annotationCount) |
void |
ClassFileReaderAdapter.setAnnotationCount(ClassFile cf,
Object tag,
int annotationCount) |
void |
ClassFileReader.setAnnotationCount(ClassFile cf,
Object tag,
int annotationCount) |
void |
ClassFileParser.setAnnotationsDone(ClassFile cf,
Object tag) |
void |
ClassFilePrinter.setAnnotationsDone(ClassFile cf,
Object tag) |
void |
ClassFileReaderAdapter.setAnnotationsDone(ClassFile cf,
Object tag) |
void |
ClassFileReader.setAnnotationsDone(ClassFile cf,
Object tag) |
void |
ClassFileParser.setAnnotationValueCount(ClassFile cf,
Object tag,
int annotationIndex,
int nValuePairs) |
void |
ClassFilePrinter.setAnnotationValueCount(ClassFile cf,
Object tag,
int annotationIndex,
int nValuePairs) |
void |
ClassFileReaderAdapter.setAnnotationValueCount(ClassFile cf,
Object tag,
int annotationIndex,
int annotationCount) |
void |
ClassFileReader.setAnnotationValueCount(ClassFile cf,
Object tag,
int annotationIndex,
int nValuePairs) |
void |
JVMAnnotationParser.setAnnotationValueElementCount(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int elementCount) |
void |
ClassFileParser.setAnnotationValueElementCount(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int elementCount) |
void |
ClassFilePrinter.setAnnotationValueElementCount(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int elementCount) |
void |
ClassFileReaderAdapter.setAnnotationValueElementCount(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int elementCount) |
void |
ClassFileReader.setAnnotationValueElementCount(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int elementCount) |
void |
JVMAnnotationParser.setAnnotationValueElementsDone(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName) |
void |
ClassFileParser.setAnnotationValueElementsDone(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName) |
void |
ClassFilePrinter.setAnnotationValueElementsDone(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName) |
void |
ClassFileReaderAdapter.setAnnotationValueElementsDone(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName) |
void |
ClassFileReader.setAnnotationValueElementsDone(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName) |
void |
ClassFilePrinter.setAnnotationValuesDone(ClassFile cf,
Object tag,
int annotationIndex) |
void |
ClassFileReaderAdapter.setAnnotationValuesDone(ClassFile cf,
Object tag,
int annotationIndex) |
void |
ClassFileReader.setAnnotationValuesDone(ClassFile cf,
Object tag,
int annotationIndex) |
void |
ClassFile.setAnnotationValuesDone(ClassFileReader reader,
Object tag,
int annotationIndex) |
void |
JVMDirectCallStackFrame.setArgument(int argIdx,
int v,
Object attr) |
void |
JVMStackFrame.setArgumentLocal(int idx,
int v,
Object attr) |
void |
JVMDirectCallStackFrame.setArgumentLocal(int argIdx,
int v,
Object attr) |
void |
JVMAnnotationParser.setClassAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String typeName) |
void |
ClassFileParser.setClassAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String typeName) |
void |
ClassFilePrinter.setClassAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String typeName) |
void |
ClassFileReaderAdapter.setClassAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String typeName) |
void |
ClassFileReader.setClassAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String typeName) |
void |
ClassFileParser.setCode(ClassFile cf,
Object tag,
int maxStack,
int maxLocals,
int codeLength) |
void |
ClassFilePrinter.setCode(ClassFile cf,
Object tag,
int maxStack,
int maxLocals,
int codeLength) |
void |
ClassFileReaderAdapter.setCode(ClassFile cf,
Object tag,
int maxStack,
int maxLocals,
int codeLength) |
void |
ClassFileReader.setCode(ClassFile cf,
Object tag,
int maxStack,
int maxLocals,
int codeLength) |
void |
ClassFileParser.setCodeAttribute(ClassFile cf,
Object tag,
int attrIndex,
String name,
int attrLength) |
void |
ClassFilePrinter.setCodeAttribute(ClassFile cf,
Object tag,
int attrIndex,
String name,
int attrLength) |
void |
ClassFileReaderAdapter.setCodeAttribute(ClassFile cf,
Object tag,
int attrIndex,
String name,
int attrLength) |
void |
ClassFileReader.setCodeAttribute(ClassFile cf,
Object tag,
int attrIndex,
String name,
int attrLength) |
void |
ClassFilePrinter.setCodeAttributeCount(ClassFile cf,
Object tag,
int attrCount) |
void |
ClassFileReaderAdapter.setCodeAttributeCount(ClassFile cf,
Object tag,
int attrCount) |
void |
ClassFileReader.setCodeAttributeCount(ClassFile cf,
Object tag,
int attrCount) |
void |
ClassFilePrinter.setCodeAttributesDone(ClassFile cf,
Object tag) |
void |
ClassFileReaderAdapter.setCodeAttributesDone(ClassFile cf,
Object tag) |
void |
ClassFileReader.setCodeAttributesDone(ClassFile cf,
Object tag) |
void |
ClassFileParser.setConstantValue(ClassFile cf,
Object tag,
Object constVal) |
void |
ClassFilePrinter.setConstantValue(ClassFile cf,
Object tag,
Object value) |
void |
ClassFileReaderAdapter.setConstantValue(ClassFile cf,
Object tag,
Object value) |
void |
ClassFileReader.setConstantValue(ClassFile cf,
Object tag,
Object value) |
void |
ClassFileParser.setEnclosingMethod(ClassFile cf,
Object tag,
String enclosingClassName,
String enclosingMethodName,
String descriptor) |
void |
ClassFilePrinter.setEnclosingMethod(ClassFile cf,
Object tag,
String enclosingClass,
String enclosingMethod,
String descriptor) |
void |
ClassFileReaderAdapter.setEnclosingMethod(ClassFile cf,
Object tag,
String enclosingClass,
String enclosingMethod,
String descriptor) |
void |
ClassFileReader.setEnclosingMethod(ClassFile cf,
Object tag,
String enclosingClass,
String enclosingMethod,
String descriptor) |
void |
JVMAnnotationParser.setEnumAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String enumType,
String enumValue) |
void |
ClassFileParser.setEnumAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String enumType,
String enumValue) |
void |
ClassFilePrinter.setEnumAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String enumType,
String enumValue) |
void |
ClassFileReaderAdapter.setEnumAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String enumType,
String enumValue) |
void |
ClassFileReader.setEnumAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String enumType,
String enumValue) |
void |
ClassFileParser.setException(ClassFile cf,
Object tag,
int exceptionIndex,
String exceptionType) |
void |
ClassFilePrinter.setException(ClassFile cf,
Object tag,
int exceptionIndex,
String exceptionType) |
void |
ClassFileReaderAdapter.setException(ClassFile cf,
Object tag,
int exceptionIndex,
String exceptionType) |
void |
ClassFileReader.setException(ClassFile cf,
Object tag,
int exceptionIndex,
String exceptionType) |
void |
ClassFileParser.setExceptionCount(ClassFile cf,
Object tag,
int exceptionCount) |
void |
ClassFilePrinter.setExceptionCount(ClassFile cf,
Object tag,
int exceptionCount) |
void |
ClassFileReaderAdapter.setExceptionCount(ClassFile cf,
Object tag,
int exceptionCount) |
void |
ClassFileReader.setExceptionCount(ClassFile cf,
Object tag,
int exceptionCount) |
void |
ClassFileParser.setExceptionHandler(ClassFile cf,
Object tag,
int handlerIndex,
int startPc,
int endPc,
int handlerPc,
String catchType) |
void |
ClassFilePrinter.setExceptionHandler(ClassFile cf,
Object tag,
int exceptionIndex,
int startPc,
int endPc,
int handlerPc,
String catchType) |
void |
ClassFileReaderAdapter.setExceptionHandler(ClassFile cf,
Object tag,
int exceptionIndex,
int startPc,
int endPc,
int handlerPc,
String catchType) |
void |
ClassFileReader.setExceptionHandler(ClassFile cf,
Object tag,
int exceptionIndex,
int startPc,
int endPc,
int handlerPc,
String catchType) |
void |
ClassFileParser.setExceptionHandlerTableCount(ClassFile cf,
Object tag,
int exceptionTableCount) |
void |
ClassFilePrinter.setExceptionHandlerTableCount(ClassFile cf,
Object tag,
int exceptionTableCount) |
void |
ClassFileReaderAdapter.setExceptionHandlerTableCount(ClassFile cf,
Object tag,
int exceptionTableCount) |
void |
ClassFileReader.setExceptionHandlerTableCount(ClassFile cf,
Object tag,
int exceptionTableCount) |
void |
ClassFileParser.setExceptionHandlerTableDone(ClassFile cf,
Object tag) |
void |
ClassFilePrinter.setExceptionHandlerTableDone(ClassFile cf,
Object tag) |
void |
ClassFileReaderAdapter.setExceptionHandlerTableDone(ClassFile cf,
Object tag) |
void |
ClassFileReader.setExceptionHandlerTableDone(ClassFile cf,
Object tag) |
void |
ClassFileParser.setExceptionsDone(ClassFile cf,
Object tag) |
void |
ClassFilePrinter.setExceptionsDone(ClassFile cf,
Object tag) |
void |
ClassFileReaderAdapter.setExceptionsDone(ClassFile cf,
Object tag) |
void |
ClassFileReader.setExceptionsDone(ClassFile cf,
Object tag) |
void |
ClassFileParser.setInnerClass(ClassFile cf,
Object tag,
int innerClsIndex,
String outerName,
String innerName,
String innerSimpleName,
int accessFlags) |
void |
ClassFilePrinter.setInnerClass(ClassFile cf,
Object tag,
int innerClsIndex,
String outerName,
String innerName,
String innerSimpleName,
int accessFlags) |
void |
ClassFileReaderAdapter.setInnerClass(ClassFile cf,
Object tag,
int innerClsIndex,
String outerName,
String innerName,
String innerSimpleName,
int accessFlags) |
void |
ClassFileReader.setInnerClass(ClassFile cf,
Object tag,
int innerClsIndex,
String outerName,
String innerName,
String innerSimpleName,
int accessFlags) |
void |
ClassFileParser.setInnerClassCount(ClassFile cf,
Object tag,
int classCount) |
void |
ClassFilePrinter.setInnerClassCount(ClassFile cf,
Object tag,
int innerClsCount) |
void |
ClassFileReaderAdapter.setInnerClassCount(ClassFile cf,
Object tag,
int innerClsCount) |
void |
ClassFileReader.setInnerClassCount(ClassFile cf,
Object tag,
int innerClsCount) |
void |
ClassFileParser.setInnerClassesDone(ClassFile cf,
Object tag) |
void |
ClassFilePrinter.setInnerClassesDone(ClassFile cf,
Object tag) |
void |
ClassFileReaderAdapter.setInnerClassesDone(ClassFile cf,
Object tag) |
void |
ClassFileReader.setInnerClassesDone(ClassFile cf,
Object tag) |
void |
ClassFileParser.setLineNumber(ClassFile cf,
Object tag,
int lineIndex,
int lineNumber,
int startPc) |
void |
ClassFilePrinter.setLineNumber(ClassFile cf,
Object tag,
int lineIndex,
int lineNumber,
int startPc) |
void |
ClassFileReaderAdapter.setLineNumber(ClassFile cf,
Object tag,
int lineIndex,
int lineNumber,
int startPc) |
void |
ClassFileReader.setLineNumber(ClassFile cf,
Object tag,
int lineIndex,
int lineNumber,
int startPc) |
void |
ClassFileParser.setLineNumberTableCount(ClassFile cf,
Object tag,
int lineNumberCount) |
void |
ClassFilePrinter.setLineNumberTableCount(ClassFile cf,
Object tag,
int lineNumberCount) |
void |
ClassFileReaderAdapter.setLineNumberTableCount(ClassFile cf,
Object tag,
int lineNumberCount) |
void |
ClassFileReader.setLineNumberTableCount(ClassFile cf,
Object tag,
int lineNumberCount) |
void |
ClassFileParser.setLineNumberTableDone(ClassFile cf,
Object tag) |
void |
ClassFilePrinter.setLineNumberTableDone(ClassFile cf,
Object tag) |
void |
ClassFileReaderAdapter.setLineNumberTableDone(ClassFile cf,
Object tag) |
void |
ClassFileReader.setLineNumberTableDone(ClassFile cf,
Object tag) |
void |
ClassFileParser.setLocalVar(ClassFile cf,
Object tag,
int localVarIndex,
String varName,
String descriptor,
int scopeStartPc,
int scopeEndPc,
int slotIndex) |
void |
ClassFilePrinter.setLocalVar(ClassFile cf,
Object tag,
int localVarIndex,
String varName,
String descriptor,
int scopeStartPc,
int scopeEndPc,
int slotIndex) |
void |
ClassFileReaderAdapter.setLocalVar(ClassFile cf,
Object tag,
int localVarIndex,
String varName,
String descriptor,
int scopeStartPc,
int scopeEndPc,
int slotIndex) |
void |
ClassFileReader.setLocalVar(ClassFile cf,
Object tag,
int localVarIndex,
String varName,
String descriptor,
int scopeStartPc,
int scopeEndPc,
int slotIndex) |
void |
ClassFileParser.setLocalVarTableCount(ClassFile cf,
Object tag,
int localVarCount) |
void |
ClassFilePrinter.setLocalVarTableCount(ClassFile cf,
Object tag,
int localVarCount) |
void |
ClassFileReaderAdapter.setLocalVarTableCount(ClassFile cf,
Object tag,
int localVarCount) |
void |
ClassFileReader.setLocalVarTableCount(ClassFile cf,
Object tag,
int localVarCount) |
void |
ClassFileParser.setLocalVarTableDone(ClassFile cf,
Object tag) |
void |
ClassFilePrinter.setLocalVarTableDone(ClassFile cf,
Object tag) |
void |
ClassFileReaderAdapter.setLocalVarTableDone(ClassFile cf,
Object tag) |
void |
ClassFileReader.setLocalVarTableDone(ClassFile cf,
Object tag) |
void |
JVMDirectCallStackFrame.setLongArgument(int argIdx,
long v,
Object attr) |
void |
JVMStackFrame.setLongArgumentLocal(int idx,
long v,
Object attr) |
void |
JVMDirectCallStackFrame.setLongArgumentLocal(int argIdx,
long v,
Object attr) |
void |
ClassFileParser.setParameterAnnotation(ClassFile cf,
Object tag,
int annotationIndex,
String annotationType) |
void |
ClassFilePrinter.setParameterAnnotation(ClassFile cf,
Object tag,
int annotationIndex,
String annotationType) |
void |
ClassFileReaderAdapter.setParameterAnnotation(ClassFile cf,
Object tag,
int annotationIndex,
String annotationType) |
void |
ClassFileReader.setParameterAnnotation(ClassFile cf,
Object tag,
int annotationIndex,
String annotationType) |
void |
ClassFileParser.setParameterAnnotationCount(ClassFile cf,
Object tag,
int paramIndex,
int annotationCount) |
void |
ClassFilePrinter.setParameterAnnotationCount(ClassFile cf,
Object tag,
int paramIndex,
int annotationCount) |
void |
ClassFileReaderAdapter.setParameterAnnotationCount(ClassFile cf,
Object tag,
int paramIndex,
int annotationCount) |
void |
ClassFileReader.setParameterAnnotationCount(ClassFile cf,
Object tag,
int paramIndex,
int annotationCount) |
void |
ClassFilePrinter.setParameterAnnotationsDone(ClassFile cf,
Object tag,
int paramIndex) |
void |
ClassFileReaderAdapter.setParameterAnnotationsDone(ClassFile cf,
Object tag,
int paramIndex) |
void |
ClassFileReader.setParameterAnnotationsDone(ClassFile cf,
Object tag,
int paramIndex) |
void |
ClassFileParser.setParameterCount(ClassFile cf,
Object tag,
int parameterCount) |
void |
ClassFilePrinter.setParameterCount(ClassFile cf,
Object tag,
int parameterCount) |
void |
ClassFileReaderAdapter.setParameterCount(ClassFile cf,
Object tag,
int parameterCount) |
void |
ClassFileReader.setParameterCount(ClassFile cf,
Object tag,
int parameterCount) |
void |
ClassFileParser.setParametersDone(ClassFile cf,
Object tag) |
void |
ClassFilePrinter.setParametersDone(ClassFile cf,
Object tag) |
void |
ClassFileReaderAdapter.setParametersDone(ClassFile cf,
Object tag) |
void |
ClassFileReader.setParametersDone(ClassFile cf,
Object tag) |
void |
JVMAnnotationParser.setPrimitiveAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
Object val) |
void |
ClassFileParser.setPrimitiveAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
Object val) |
void |
ClassFilePrinter.setPrimitiveAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
Object val) |
void |
ClassFileReaderAdapter.setPrimitiveAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
Object val) |
void |
ClassFileReader.setPrimitiveAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
Object val) |
void |
JVMDirectCallStackFrame.setReferenceArgument(int argIdx,
int ref,
Object attr) |
void |
JVMStackFrame.setReferenceArgumentLocal(int idx,
int ref,
Object attr) |
void |
JVMDirectCallStackFrame.setReferenceArgumentLocal(int argIdx,
int v,
Object attr) |
void |
ClassFileParser.setSignature(ClassFile cf,
Object tag,
String signature) |
void |
ClassFilePrinter.setSignature(ClassFile cf,
Object tag,
String signature) |
void |
ClassFileReaderAdapter.setSignature(ClassFile cf,
Object tag,
String signature) |
void |
ClassFileReader.setSignature(ClassFile cf,
Object tag,
String signature) |
void |
ClassFile.setSignature(ClassFileReader reader,
Object tag,
String signature) |
void |
ClassFileParser.setSourceFile(ClassFile cf,
Object tag,
String fileName) |
void |
ClassFilePrinter.setSourceFile(ClassFile cf,
Object tag,
String pathName) |
void |
ClassFileReaderAdapter.setSourceFile(ClassFile cf,
Object tag,
String pathName) |
void |
ClassFileReader.setSourceFile(ClassFile cf,
Object tag,
String pathName) |
void |
JVMAnnotationParser.setStringAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String val) |
void |
ClassFileParser.setStringAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String val) |
void |
ClassFilePrinter.setStringAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String s) |
void |
ClassFileReaderAdapter.setStringAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String s) |
void |
ClassFileReader.setStringAnnotationValue(ClassFile cf,
Object tag,
int annotationIndex,
int valueIndex,
String elementName,
int arrayIndex,
String s) |
Modifier and Type | Class and Description |
---|---|
class |
AALOAD
Load reference from array
..., arrayref, index => ..., value
|
class |
AASTORE
Store into reference array
..., arrayref, index, value => ...
|
class |
ACONST_NULL
Push null
...
|
class |
ALOAD
Load reference from local variable
...
|
class |
ANEWARRAY
Create new array of reference
..., count => ..., arrayref
|
class |
ARETURN
Return reference from method
..., objectref => [empty]
|
class |
ArrayElementInstruction
abstract class for operations that access elements of arrays
|
class |
ArrayInstruction
abstraction for all array instructions
|
class |
ARRAYLENGTH
Get length of array
..., arrayref => ..., length
|
class |
ArrayLoadInstruction
abstraction for all array load instructions
..., array, index => ..., value
|
class |
ArrayStoreInstruction
abstraction for all array store instructions
...
|
class |
ASTORE
Store reference into local variable
..., objref => ...
|
class |
ATHROW
Throw exception or error
..., objectref => objectref
|
class |
BALOAD
Load byte or boolean from array
..., arrayref, index => ..., value
|
class |
BASTORE
Store into byte or boolean array
..., arrayref, index, value => ...
|
class |
BIPUSH
Push byte
...
|
class |
CALOAD
Load char from array
..., arrayref, index => ..., value
|
class |
CASTORE
Store into char array
..., arrayref, index, value => ...
|
class |
CHECKCAST
Check whether object is of given type
..., objectref => ..., objectref
|
class |
D2F
Convert double to float
..., value => ..., result
|
class |
D2I
Convert double to int
..., value => ..., result
|
class |
D2L
Convert double to long
..., value => ..., result
|
class |
DADD
Add double
..., value1, value2 => ..., result
|
class |
DALOAD
Load double from array
..., arrayref, index => ..., value
|
class |
DASTORE
Store into double array
..., arrayref, index, value => ...
|
class |
DCMPG
Compare double
..., value1, value2 => ..., result
|
class |
DCMPL
Compare double
..., value1, value2 => ..., result
|
class |
DCONST
Push double
...
|
class |
DDIV
Divide double
..., value1, value2 => ..., result
|
class |
DIRECTCALLRETURN
this is used to return from a DirectCallStackFrame
Note that it is NOT a ReturnInstruction, in case listeners monitor these
and expect corresponding InvokeInstructions.
|
class |
DLOAD
Load double from local variable
...
|
class |
DMUL
Multiply double
..., value1, value2 => ..., result
|
class |
DNEG
Negate double
..., value => ..., result
|
class |
DoubleCompareInstruction
base class for double double compare instructions
|
class |
DREM
Remainder double
..., value1, value2 => ..., result
|
class |
DRETURN
Return double from method
..., value => [empty]
|
class |
DSTORE
Store double into local variable
..., value => ...
|
class |
DSUB
Subtract double
..., value1, value2 => ..., result
|
class |
DUP
duplicate topmost stack entry
.., value -> .., value, value
|
class |
DUP_X1
Duplicate the top operand stack value and insert two values down
..., value2, value1 => ..., value1, value2, value1
|
class |
DUP_X2
DOCUMENT ME!
|
class |
DUP2
Duplicate the top one or two operand stack values
..., value2, value1 => ..., value2, value1, value2, value1
|
class |
DUP2_X1
DOCUMENT ME!
|
class |
DUP2_X2
Duplicate the top operand stack value and insert two or three values down
...
|
class |
EXECUTENATIVE
this is a synthetic instruction to (re-)execute native methods
Note that StackFrame and lock handling has to occur from within
the corresponding NativeMethodInfo
|
class |
F2D
Convert float to double
..., value => ..., result
|
class |
F2I
Convert float to int
..., value => ..., result
|
class |
F2L
Convert float to long
..., value => ..., result
|
class |
FADD
Add float
..., value1, value2 => ..., result
|
class |
FALOAD
Load float from array
..., arrayref, index => ..., value
|
class |
FASTORE
Store into float array
..., arrayref, index, value => ...
|
class |
FCMPG
Compare float
..., value1, value2 => ..., result
|
class |
FCMPL
Compare float
..., value1, value2 => ..., result
|
class |
FCONST
Push float
...
|
class |
FDIV
divide float
..., value1, value2 => ..., result
|
class |
FieldInstruction
parent class for PUT/GET FIELD/STATIC insns
<2do> there is a inheritance level missing to deal with instance/static
fields - w/o the instance/static helper methods we would have to duplicate
code in the getters/setters
|
class |
FLOAD
Load float from local variable
...
|
class |
FMUL
Multiply float
..., value1, value2 => ..., result
|
class |
FNEG
Negate float
..., value => ..., result
|
class |
FREM
Remainder float
..., value1, value2 => ..., result
|
class |
FRETURN
Return float from method
..., value => [empty]
|
class |
FSTORE
Store float into local variable
..., value => ...
|
class |
FSUB
Subtract float
..., value1, value2 => ..., result
|
class |
GETFIELD
Fetch field from object
..., objectref => ..., value
|
class |
GETSTATIC
Get static fieldInfo from class
..., => ..., value
|
class |
GOTO
Branch always
No change
<2do> store this as code insnIndex, not as bytecode position
|
class |
GOTO_W |
class |
I2B
Convert int to byte
..., value => ..., result
|
class |
I2C
Convert int to char
..., value => ..., result
|
class |
I2D
Convert int to double
..., value => ..., result
|
class |
I2F
Convert int to float
..., value =>..., result
|
class |
I2L
Convert int to long
..., value => ..., result
|
class |
I2S
Convert int to short
..., value => ..., result
|
class |
IADD
Add int
..., value1, value2 =>..., result
|
class |
IALOAD
Load int from array
..., arrayref, index => ..., value
|
class |
IAND
Boolean AND int
..., value1, value2 => ..., result
|
class |
IASTORE
Store into int array
..., arrayref, index, value => ...
|
class |
ICONST
Push int constant
...
|
class |
IDIV
Divide int
..., value1, value2 =>..., result
|
class |
IF_ACMPEQ
Branch if reference comparison succeeds
..., value1, value2 => ...
|
class |
IF_ACMPNE
Branch if reference comparison does not succeed
..., value1, value2 => ...
|
class |
IF_ICMPEQ
Branch if int comparison succeeds
..., value1, value2 => ...
|
class |
IF_ICMPGE
Branch if int comparison succeeds
..., value1, value2 => ...
|
class |
IF_ICMPGT
Branch if int comparison succeeds
..., value1, value2 => ...
|
class |
IF_ICMPLE
Branch if int comparison succeeds
..., value1, value2 => ...
|
class |
IF_ICMPLT
Branch if int comparison succeeds
..., value1, value2 => ...
|
class |
IF_ICMPNE
Branch if int comparison succeeds
..., value1, value2 => ...
|
class |
IFEQ
Branch if int comparison with zero succeeds
..., value => ...
|
class |
IFGE
Branch if int comparison with zero succeeds
..., value => ...
|
class |
IFGT
Branch if int comparison with zero succeeds
..., value => ...
|
class |
IfInstruction
abstraction for all comparison instructions
|
class |
IFLE
Branch if int comparison with zero succeeds
..., value => ...
|
class |
IFLT
Branch if int comparison with zero succeeds
..., value => ...
|
class |
IFNE
Branch if int comparison with zero succeeds
..., value => ...
|
class |
IFNONNULL
Branch if reference not null
..., value => ..., result
|
class |
IFNULL
DOCUMENT ME!
|
class |
IINC
Increment local variable by constant
No change
|
class |
ILOAD
Load int from local variable
...
|
class |
IMUL
Multiply int
..., value1, value2 => ..., result
|
class |
INEG
Negate int
..., value => ..., result
|
class |
InstanceFieldInstruction
class abstracting instructions that access instance fields
|
class |
InstanceInvocation
base class for INVOKEVIRTUAL, INVOKESPECIAL and INVOLEINTERFACE
|
class |
INSTANCEOF
Determine if object is of given type
..., objectref => ..., result
|
class |
InstructionFactory
this is the new JVMInstructionFactory
|
class |
InstructionVisitorAdapter |
class |
INVOKECG
a sytnthetic INVOKE instruction that gets it's parameters from an
InvocationCG.
|
class |
INVOKECLINIT
this is an artificial bytecode that we use to deal with the particularities of
|
class |
InvokeInstruction
abstraction for all invoke instructions
|
class |
INVOKEINTERFACE
Invoke interface method
..., objectref, [arg1, [arg2 ...]] => ...
|
class |
INVOKESPECIAL
Invoke instance method; special handling for superclass, private,
and instance initialization method invocations
..., objectref, [arg1, [arg2 ...]] => ...
|
class |
INVOKESTATIC
Invoke a class (static) method
..., [arg1, [arg2 ...]] => ...
|
class |
INVOKEVIRTUAL
Invoke instance method; dispatch based on class
..., objectref, [arg1, [arg2 ...]] => ...
|
class |
IOR
Boolean OR int
..., value1, value2 => ..., result
|
class |
IREM
Remainder int
..., value1, value2 => ..., result
|
class |
IRETURN
Return int from method
..., value => [empty]
|
class |
ISHL
Shift left int
..., value1, value2 => ..., result
|
class |
ISHR
Arithmetic shift right int
..., value1, value2 => ..., result
|
class |
ISTORE
Store int into local variable
..., value => ...
|
class |
ISUB
Subtract int
..., value1, value2 => ..., result
|
class |
IUSHR
Logical shift right int
..., value1, value2 => ..., result
|
class |
IXOR
Boolean XOR int
..., value1, value2 => ..., result
|
class |
JSR
Jump subroutine
...
|
class |
JSR_W
Jump subroutine (wide insnIndex)
...
|
class |
L2D
Convert long to double
..., value => ..., result
|
class |
L2F
Convert long to float
..., value => ..., result
|
class |
L2I
Convert long to int
..., value => ..., result
|
class |
LADD
Add long
..., value1, value2 => ..., result
|
class |
LALOAD
Load long from array
..., arrayref, index => ..., value
|
class |
LAND
Boolean AND long
..., value1, value2 => ..., result
|
class |
LASTORE
Store into long array
..., arrayref, index, value => ...
|
class |
LCMP
Compare long
..., value1, value2 => ..., result
|
class |
LCONST
Push long constant
...
|
class |
LDC
Push item from runtime constant pool
...
|
class |
LDC_W
Push item from runtime constant pool (wide index)
...
|
class |
LDC2_W
Push long or double from runtime constant pool (wide index)
...
|
class |
LDIV
Divide long
..., value1, value2 => ..., result
|
class |
LLOAD
Load long from local variable
...
|
class |
LMUL
Multiply long
..., value1, value2 => ..., result
|
class |
LNEG
Negate long
..., value => ..., result
|
class |
LocalVariableInstruction
class abstracting instructions that access local variables, to keep
track of slot/varname mapping
|
class |
LockInstruction
common root for MONITORENTER/EXIT
|
class |
LongArrayLoadInstruction
abstraction for long array loads
|
class |
LongArrayStoreInstruction
absraction for long array stores
...
|
class |
LongReturn
common base for DRETURN and LRETURN
|
class |
LOOKUPSWITCH
Access jump table by key match and jump
..., key => ...
|
class |
LOR
Boolean OR long
..., value1, value2 => ..., result
|
class |
LREM
Remainder long
..., value1, value2 => ..., result
|
class |
LRETURN
Return long from method
..., value => [empty]
|
class |
LSHL
Shift left
..., value1, value2 =>..., result
|
class |
LSHR
Arithmetic shift right long
..., value1, value2 =>..., result
|
class |
LSTORE
Store long into local variable
..., value => ...
|
class |
LSUB
Subtract long
..., value1, value2 => ..., result
|
class |
LUSHR
Logical shift right long
..., value1, value2 =>..., result
|
class |
LXOR
Boolean XOR long
..., value1, value2 => ..., result
|
class |
MONITORENTER
Enter monitor for object
..., objectref => ...
|
class |
MONITOREXIT
Exit monitor for object
..., objectref => ...
|
class |
MULTIANEWARRAY
Create new multidimensional array
..., count1, [count2, ...] => ..., arrayref
|
class |
NATIVERETURN
synthetic return instruction for native method invocations, so that
we don't have to do special provisions to copy the caller args in case
a post exec listener wants them.
|
class |
NEW
Create new object
...
|
class |
NEWARRAY
Create new array
..., count => ..., arrayref
|
class |
NewArrayInstruction |
class |
NOP
Do nothing
No change
|
class |
POP
Pop the top operand stack value
..., value => ...
|
class |
POP2
Pop the top two operand slots
..., value2, value1 => ...
|
class |
PUTFIELD
Set field in object
..., objectref, value => ...
|
class |
PUTSTATIC
Set static field in class
..., value => ...
|
class |
RET
Return from subroutine
No change
|
class |
RETURN
Return void from method
...
|
class |
ReturnInstruction
abstraction for the various return instructions
|
class |
RUNSTART
this is an artificial instruction that is automatically prepended to
a run()/main() method call.
|
class |
SALOAD
Load short from array
..., arrayref, index => ..., value
|
class |
SASTORE
Store into short array
..., array, index, value => ...
|
class |
SIPUSH
Push short
...
|
class |
StaticFieldInstruction
class to abstract instructions accessing static fields
|
class |
SWAP
Swap the top two operand stack values
..., value2, value1 => ..., value1, value2
|
class |
SwitchInstruction
common root class for LOOKUPSWITCH and TABLESWITCH insns
<2do> this is inefficient.
|
class |
TABLESWITCH
Access jump table by index and jump
..., index => ...
|
class |
VirtualInvocation
a base class for virtual call instructions
|
class |
WIDE
modifies following insn, no stack manipulation
NOTE: transparently handled by BCEL, we should never receive this
(1):
|
Modifier and Type | Field and Description |
---|---|
protected Object[] |
InvokeInstruction.arguments |
Modifier and Type | Method and Description |
---|---|
Object |
InstructionFactory.clone() |
Object[] |
InvokeInstruction.getArgumentAttrs(ThreadInfo ti) |
Object |
InvokeInstruction.getArgumentValue(String id,
ThreadInfo ti)
<2do> - this relies on same order of arguments and LocalVariableTable entries, which
seems to hold for javac, but is not required by the VM spec, which only
says that arguments are stored in consecutive slots starting at 0
|
Object[] |
InvokeInstruction.getArgumentValues(ThreadInfo ti)
this is a little helper to find out about call argument values from listeners that
don't want to dig through MethodInfos and Types.
|
Object |
InvokeInstruction.getFieldOrArgumentValue(String id,
ThreadInfo ti) |
Object |
VirtualInvocation.getFieldValue(String id,
ThreadInfo ti) |
abstract Object |
InvokeInstruction.getFieldValue(String id,
ThreadInfo ti) |
Object |
INVOKESPECIAL.getFieldValue(String id,
ThreadInfo ti) |
Object |
INVOKESTATIC.getFieldValue(String id,
ThreadInfo ti) |
Object |
RETURN.getReturnAttr(ThreadInfo ti) |
Object |
NATIVERETURN.getReturnAttr(ThreadInfo ti) |
Object |
ReturnInstruction.getReturnAttr(ThreadInfo ti)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
obviously, this only makes sense from an instructionExecuted(), since
the value is pushed during the enter().
|
Object |
LongReturn.getReturnAttr(ThreadInfo ti)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
obviously, this only makes sense from an instructionExecuted(), since
the value is pushed during the enter().
|
protected Object |
FRETURN.getReturnedOperandAttr(StackFrame frame) |
protected Object |
RETURN.getReturnedOperandAttr(StackFrame frame) |
protected Object |
ARETURN.getReturnedOperandAttr(StackFrame frame) |
protected Object |
NATIVERETURN.getReturnedOperandAttr(StackFrame frame) |
protected Object |
IRETURN.getReturnedOperandAttr(StackFrame frame) |
protected abstract Object |
ReturnInstruction.getReturnedOperandAttr(StackFrame frame) |
protected Object |
LongReturn.getReturnedOperandAttr(StackFrame frame) |
Object |
DRETURN.getReturnValue(ThreadInfo ti) |
Object |
RETURN.getReturnValue(ThreadInfo ti) |
Object |
ARETURN.getReturnValue(ThreadInfo ti) |
Object |
NATIVERETURN.getReturnValue(ThreadInfo ti) |
Object |
IRETURN.getReturnValue(ThreadInfo ti) |
Object |
LRETURN.getReturnValue(ThreadInfo ti) |
abstract Object |
ReturnInstruction.getReturnValue(ThreadInfo ti) |
Modifier and Type | Method and Description |
---|---|
void |
ReturnInstruction.addReturnAttr(ThreadInfo ti,
Object attr) |
void |
LongReturn.addReturnAttr(ThreadInfo ti,
Object attr) |
<T> T |
ReturnInstruction.getNextReturnAttr(ThreadInfo ti,
Class<T> type,
Object prev) |
<T> T |
LongReturn.getNextReturnAttr(ThreadInfo ti,
Class<T> type,
Object prev) |
void |
ReturnInstruction.setReturnAttr(ThreadInfo ti,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
we don't clone since pushing a return value already changed the caller frame
|
void |
LongReturn.setReturnAttr(ThreadInfo ti,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
we don't clone since pushing a return value already changed the caller frame
|
Modifier and Type | Class and Description |
---|---|
class |
AssertionProperty
this is a property listener that turns thrown AssertionErrors into
property violations before they are caught (i.e.
|
class |
BudgetChecker
Listener that implements various budget constraints
|
class |
CallMonitor
this isn't yet a useful tool, but it shows how to track method calls with
their corresponding argument values
|
class |
CGMonitor |
class |
CGRemover
listener that removes CGs for specified locations, method calls or method bodies
This is an application specific state space optimizer that should be used
carefully since it has to be aware of which CGs can be removed, and which
ones can't (e.g.
|
class |
ChoiceSelector
this is a listener that only executes single choices until it detects
that it should start to search.
|
class |
ChoiceTracker
generic choice tracker tool, to produce a list of choice values that
can be used to create readable replay scripts etc.
|
class |
CoverageAnalyzer
a listener to report coverage statistics
The idea is to collect per-class/-method/-thread information about
executed instructions, and then analyze this deeper when it comes to
report time (e.g.
|
class |
DeadlockAnalyzer
example of a listener that creates property specific traces.
|
class |
EndlessLoopDetector
little listener that tries to detect endless while() loops by counting
backjumps, breaking transitions if the count exceeds a threshold, and
then checking if program states match.
|
class |
ErrorTraceGenerator
A lightweight listener to generate the error trace by printing
the program instructions at transition boundaries.
|
class |
ExceptionInjector
listener to inject exceptions according to user specifications.
|
class |
ExecTracker
Listener tool to monitor JPF execution.
|
class |
HeapTracker
HeapTracker - property-listener class to check heap utilization along all
execution paths (e.g.
|
class |
IdleFilter
simple combined listener that checks if a thread seems to do idle loops that
might starve other threads or JPF.
|
class |
InsnCounter
simple tools to gather statistics about instructions executed by JPF.
|
class |
LockedStackDepth
A listener that tracks information about the stack depth of when a lock is first acquired.
|
class |
LogConsole
simple logging facility that listens on a socket (e.g.
|
class |
MethodAnalyzer
analyzes call/execute sequences of methods
closely modeled after the DeadlockAnalyzer, i.e.
|
class |
MethodTracker
simple tool to log method invocations
at this point, it doesn't do fancy things yet, but gives a more high
level idea of what got executed by JPF than the ExecTracker
|
class |
NoStateCycles
If there is a cycle in the states of the program, JPF doesn't execute the
already visited states.
|
class |
NumericValueChecker
little listener that checks value ranges of specified numeric fields and local vars
configuration examples:
range.fields=speed,..
|
class |
ObjectTracker
listener that keeps track of all allocations, method calls, field updates
and deallocations of instances of a set of types
we don't need a StateExtensionClient/Listener here because we only
keep live, typed object data.
|
class |
OOMEInjector
simulator for OutOfMemoryErrors.
|
class |
OverlappingMethodAnalyzer
this is a specialized MethodAnalyzer that looks for overlapping method
calls on the same object from different threads.
|
class |
PathOutputMonitor
listener that monitors path output, matching it against specifications
supplied as text files.
|
class |
Perturbator
listener that perturbs GETFIELD/GETSTATIC and InvokeInstruction results
NOTE - this listener initializes in two steps: (1) during listener construction
it builds a list of classes it has to monitor, and (2) during class load
time it further analyzes classes from this list to get the actual target
objects (FieldInfos and MethodInfos) so that instruction monitoring is
efficient enough.
|
static class |
Perturbator.FieldPerturbation |
static class |
Perturbator.ParamsPerturbation |
static class |
Perturbator.Perturbation |
static class |
Perturbator.ReturnPerturbation |
class |
PreciseRaceDetector
This is a Race Detection Algorithm that is precise in its calculation of races, i.e.
|
class |
ReferenceLocator
tiny utility listener that can be used to find out where a certain
object (specified by reference) gets allocated or accessed (call or field),
and when it gets gc'ed
|
class |
SearchMonitor
SearchListener class to collect and report statistical
data during JPF execution.
|
class |
SearchStats
An alternative to SearchMonitor that just reports statistics at the end.
|
class |
SimpleDot
an alternative Graphviz dot-file generator for simple,educational state graphs
except of creating funny wallpapers, it doesn't help much in real life if the
state count gets > 50, but for the small ones it's actually quite readable.
|
class |
SimpleIdleFilter
This is the simple version of IdleFilter.
|
class |
StackDepthChecker
listener that throws a java.lang.StackOverflowError in case a thread
exceeds a configured max stack depth
<2do> - maybe we should only count visible stackframes, i.e.
|
class |
StackTracker
simple tool to log stack invocations
at this point, it doesn't do fancy things yet, but gives a more high
level idea of what got executed by JPF than the ExecTracker
|
class |
StateCountEstimator
From already visited states, estimates the total number of states by the branching factor.
|
class |
StateSpaceAnalyzer
a listener that collects information about ChoiceGenerators, choices and
where they are used.
|
class |
StateSpaceDot |
class |
StateTracker
simple tool to log state changes
|
class |
StopWatchFuzzer
a listener that is used to explore all paths from a time-value comparison.
|
class |
TraceStorer
tool to save traces upon various conditions like
- property violation
- call of a certain method
- reaching a certain search depth
- creating a certain thread
|
class |
VarRecorder
Simple listener tool to record the values of variables as they are accessed.
|
class |
VarTracker
simple listener tool to find out which variables (locals and fields) are
changed how often and from where.
|
Modifier and Type | Class and Description |
---|---|
class |
GenericDataAbstractor
This file implements a generic data abstraction module that can be used
with the Perturbator to execute a method with a choice of values for the
method parameters.
|
class |
GenericDataAbstractor.Valuation |
class |
IntOverUnder
simple +/- delta perturbation of integer operand values
|
Modifier and Type | Method and Description |
---|---|
ChoiceGenerator<?> |
OperandPerturbator.createChoiceGenerator(String id,
StackFrame frame,
Object refObject) |
ChoiceGenerator<?> |
GenericDataAbstractor.createChoiceGenerator(String id,
StackFrame frame,
Object refObject) |
ChoiceGenerator<?> |
IntOverUnder.createChoiceGenerator(String id,
StackFrame frame,
Object refObject) |
Modifier and Type | Class and Description |
---|---|
class |
ConsolePublisher |
class |
Publisher
abstract base for all format specific publishers.
|
class |
PublisherExtensionAdapter
this is just a little helper class to ease standalone PublisherExtension implementations
|
class |
Reporter
this is our default report generator, which is heavily configurable
via our standard properties.
|
class |
Statistics
simple structure to hold statistics info created by Reporters/Publishers
this is kind of a second tier SearchListener, which does not
explicitly have to be registered
<2do> this should get generic and accessible enough to replace all the
other statistics collectors, otherwise there is too much redundancy.
|
class |
XMLPublisher |
Modifier and Type | Class and Description |
---|---|
class |
DFSearch
standard depth first model checking (but can be bounded by search depth
and/or explicit Verify.ignoreIf)
|
class |
PathSearch
PathSearch is not really a Search object, just a simple 'forward'
driver for the VM that loops until there is no next instruction or
a property doesn't hold
|
class |
RandomSearch
this is a straight execution pseudo-search - it doesn't search at
all (i.e.
|
class |
Search
the mother of all search classes.
|
class |
SearchListenerAdapter
a no-action SearchListener which we can use to override only the
notifications we are interested in
|
class |
SearchState |
class |
Simulation
this is a straight execution pseudo-search - it doesn't search at
all (i.e.
|
Modifier and Type | Class and Description |
---|---|
class |
BFSHeuristic
breadth first search
|
class |
DFSHeuristic
heuristic state prioritizer that favors search depth
|
class |
GlobalSwitchThread
heuristic state prioritizer that tries to minimize re-scheduling
|
class |
HeuristicSearch
a search strategy class that computes all immediate successors of a given
state, puts them into a priority queue (the priority is provided by a
Heuristic strategy object), and processes states in the sequence of
highest priorities.
|
class |
HeuristicState
wrapper for states that are processed in an order that is
defined by a heuristic (i.e.
|
class |
Interleaving
Heuristic to maximize thread interleavings.
|
class |
MinimizePreemption
a simple heuristic that tries to minimize preemptive scheduling, i.e.
|
class |
MostBlocked
Heuristic state prioriizer that maximizes number of blocked states.
|
class |
PreferThreads
a heuristic state prioritizer that favors certain threads (specified
by thread names during initialization)
<2do> for both efficiency and encapsulation reasons, this should be just
a Scheduler policy (so that we don't have to expand all children)
|
class |
PrioritizedState
HeuristicState with a scalar, static priority.
|
class |
RandomHeuristic
heuristic state prioritizer that returns random priority values
|
class |
SimplePriorityHeuristic
a heuristic that is based on static priorities that are determined
at state storage time
|
class |
StaticPriorityQueue
container for statically prioritized states, based on bounded
RB trees
TreeSet is a better choice than PriorityQueue since the size
constraint means we have to remove elements from both ends, which
is inefficient with heaps.
|
class |
UserHeuristic
heuristic state prioritizer that uses fields of the Main class under test
to determine priorities (i.e.
|
Modifier and Type | Method and Description |
---|---|
boolean |
PrioritizedState.equals(Object o) |
Modifier and Type | Class and Description |
---|---|
class |
GenPeer
tool to automatically generate the framework of a native peer MJI class,
given it's model class.
|
class |
Run
common base for Run* classes
|
class |
RunAnt
starter class to use the (minimal) ant installation that comes with
jpf-core
|
class |
RunJPF
This class is a wrapper for loading JPF or a JPFShell through a classloader
that got initialized from a Config object (i.e.
|
class |
RunTest
tool to run JPF test with configured classpath
arguments are supposed to be of type
{
|
static class |
RunTest.Failed |
Modifier and Type | Method and Description |
---|---|
protected static boolean |
Run.call(Class<?> cls,
String mthName,
Object[] args) |
Modifier and Type | Class and Description |
---|---|
class |
ArrayIntSet
common base for array based IntSet implementations
|
class |
ArrayObjectQueue<E>
dynamically growing, cyclic array buffer queue for object references
|
class |
AvailableBufferedInputStream |
class |
BitArray
Faster version of BitSet for fixed size.
|
class |
BitSet1024
a fixed size BitSet with 1024 bits.
|
class |
BitSet256
a fixed size BitSet with 256 bits.
|
class |
BitSet64 |
class |
CommitOutputStream |
class |
ConsoleStream
a utility that can be used to write logs which are displayed in a JTextArea
|
class |
ConstGrowth |
class |
Debug
logger used to print debugging messages based on the required debug level and
message category.
|
class |
DynamicIntArray
simplistic dynamic array that differentiates from ArrayList by
- using chunks instead of exponential growth, thus efficiently dealing
with sparse arrays
- managing primitive 'int' types, i.e.
|
class |
DynamicObjectArray<E>
simplistic Object array that differentiates from ArrayList by
using chunks instead of exponential growth, thus efficiently dealing
with huge, potentially sparse arrays
the motivation for this class is memory optimization, i.e.
|
class |
ExpGrowth |
class |
FeatureSpec
common base class for MethodSpec and FieldSpec
|
class |
FieldSpec
utility class that can match FieldInfos against specs.
|
class |
FileUtils
utility class to find all files matching (possibly hierarchical)
wildcard path specs
we support single '*' wildcards as in filename matching, plus "**" patterns
that match all (recursive) subdirectories
|
class |
FinalBitSet
Faster version of BitSet for those that never change.
|
class |
HashData
object to compute complex hash values that can be accumulated and
delegated (to aggregates etc.)
used to obtain hashcodes for states
|
class |
HashPool<V>
data structure used to do hash collapsing.
|
class |
IdentityArrayObjectSet<E>
simple identity set for objects
we don't sort&bisect, assuming the number of entries will be small
be aware this doesn't scale to large sets
|
class |
ImmutableList<E>
utility class for JPF internal linked lists that are tail-immutable
|
class |
InstructionFactoryFilter
utility class that can be used by InstructionFactory implementations to
selectively replace bytecodes for specified class sets.
|
class |
IntArray
Wrapper for int[] that provides proper equals() and hashCode() methods.
|
class |
IntTable<E>
A hash map that holds int values associated with generic key objects.
|
static class |
IntTable.Entry<E>
encapsulates an Entry in the table.
|
static class |
IntTable.Snapshot<E>
helper class to store a compact, invariant representation of this table
|
protected class |
IntTable.TblIterator |
class |
IntVector
(more efficient?) alternative to Vector
|
class |
Invocation
a record that includes all information to perform a call
|
class |
JPFLogger
this is a decorator for java.util.logging.JPFLogger
We use this to avoid explicit Logger.isLoggable() checks in the code.
|
class |
JPFSiteUtils
utility class for JPF site configuration related functions.
|
class |
Left
left justified output
<2do> this is not worth a class! use a general TextFormatter
|
class |
LimitedInputStream |
class |
LinkedObjectQueue<E>
object queue that uses cached link entries
|
class |
LocationSpec
support for specification of source locations
This maps sourcefile:line1-range strings into instructions that can be efficiently
checked for by listeners.
|
class |
LogHandler
log handler class that deals with output selection and formatting.
|
static class |
LogHandler.DefaultConsoleHandler |
class |
LogManager
this class is responsible for returning properly JPF-configured
Loggers.
|
class |
LongVector
(more efficient?) alternative to Vector
|
class |
MethodInfoRegistry
just a little helper for java.lang.reflect peers
<2do> - it's overly simplistic for now
|
class |
MethodSpec
utility class that can match methods/args against specs.
|
class |
Misc |
class |
MutableInteger
an object that holds a mutable int.
|
class |
MutableIntegerRestorer
on-demand restorer for MutableInteger instances
|
class |
OATHash
Bob Jenkins One-at-a-Time Hash (http://www.burtleburtle.net/bob/hash/doobs.html),
a simple yet sufficiently avalanching hash that doesn't require a-priori knowledge
of the key length and is much faster than lookup3
|
class |
ObjArray<E>
Wrapper for arrays of objects which provides proper equals() and hashCode()
methods, and behaves nicely with Java 1.5 generics.
|
class |
ObjectConverter
Object transformer from Java objects to JPF objects
|
class |
ObjectList
a minimal container API that transparently handles Object lists which can
degenerate to single values that are stored directly.
|
static class |
ObjectList.Iterator |
static class |
ObjectList.TypedIterator<A> |
class |
ObjVector<E>
more customizable alternative to java.util.Vector.
|
static class |
ObjVector.MutatingSnapshot<E,T>
snapshot that can mutate element values, but therefore can't use block operations.
|
protected class |
ObjVector.NonNullIterator
iterator that only includes element values that are not null
|
protected class |
ObjVector.OVIterator
iterator that goes over all elements regardless of value (i.e.
|
static class |
ObjVector.Snapshot<E>
this is a block operation snapshot that stores chunks of original data with
not more than DEFAULT_MAX_GAP consecutive null elements.
|
class |
Pair<A,B>
simple const wrapper utility class for 2-tuple
|
class |
PathnameExpander
utility to perform pathname expansion
the following patterns are supported so far:
(1) brace expansion ala bash: foo{Boo,Shoo} => fooBoo, fooShoo
(this doesn't check for existence, its simply lexical)
(2) '*' wildcard pathname expansion ala bash: "*.java" | "*\Main*.java"
(supports wildcards in mutiple path elements and within file/dir name)
(3) recursive dir expansion ala Ant: "**\*.jar"
|
class |
Permutation |
class |
PrintUtils |
class |
PSIntMap<V>
Persistent (immutable) associative array that maps integer keys to generic reference values.
|
protected static class |
PSIntMap.BitmapNode<E>
A node that holds between 2 and 31 elements.
|
protected static class |
PSIntMap.FullNode<E>
newElements node with 32 elements, for which we don't need newElements bitmap.
|
protected static class |
PSIntMap.Node<E>
Abstract root class for all node types.
|
protected static class |
PSIntMap.OneNode<E>
Node that has only one element and hence does not need an array.
|
protected class |
PSIntMap.ValueIterator
this is less efficient than using map.process(processor), but required to use PSIntMaps in lieu of ordinary containers
Since PSIntMaps are bounded recursive data structures, we have to model newElements stack explicitly, but at least we know it is
not exceeding newElements depth of 6 (5 bit index blocks)
Note - there are no empty nodes.
|
class |
Reflection
reflection utilities
|
class |
RepositoryEntry
simple generic structure to hold repository info for source files
<2do> extend this to find out what the status of the repository is, i.e.
|
class |
Result
simple result wrapper that can store a boolean value and a String, to
be used as method return value if we have to keep exceptions in the callee
|
class |
Right
right justified output
<2do> this is not worth a class! use a general TextFormatter
|
class |
RunRegistry
little helper to enable resetting classes and objects between JPF runs,
mostly to avoid memory leaks
reset() has to be called at the beginning of a new run, causing all
still registered listeners to be notified.
|
class |
SimplePool<E>
This is a simplified hash pool that does not support removal or
numbering of elements.
|
class |
SortedArrayIntSet
a set of integers that uses a simple sorted int array and binary search
To be used in a context where
- the number of elements does not have a hard limit
- the number of elements is assumed to be small, but potentially sparse
- the following operations are time critical
+ inclusion check
+ size check
+ cloning
+ iteration over elements
- adding/removing should be better than O(N)
|
class |
SortedArrayObjectSet<T extends Comparable<T>>
a generic set of comparable objects with value based inclusion check
(i.e.
|
class |
Source
utility class to access arbitrary source files by line number
sources can be files inside of root directories, or
can be entries in jars
|
class |
SourceRef
a source reference abstraction wrapping file and line information
|
class |
SparseClusterArray<E>
A generic sparse reference array that assumes clusters, and more
frequent intra-cluster access.
|
protected static class |
SparseClusterArray.Chunk |
protected static class |
SparseClusterArray.ChunkNode |
protected class |
SparseClusterArray.ElementIndexIterator |
protected class |
SparseClusterArray.ElementIterator<T> |
static class |
SparseClusterArray.Entry<E> |
protected static class |
SparseClusterArray.Node
this corresponds to a toplevel cluster (e.g.
|
protected static class |
SparseClusterArray.Root |
static class |
SparseClusterArray.Snapshot<T,E> |
class |
SparseIntVector
This has approximately the interface of IntVector but uses a hash table
instead of an array.
|
static class |
SparseIntVector.Snapshot
a simplistic snapshot implementation that stores set indices/values in order to save space
|
class |
SparseObjVector<E>
This has approximately the interface of ObjVector but uses a hash table
instead of an array.
|
class |
SplitInputStream |
class |
SplitOutputStream |
class |
StateExtensionListener<T>
generic listener that keeps track of state extensions, using
state ids as index values into a dynamic array of T objects
the purpose of this utility class is to make state extensions
backtrackable, so that clients don't have to care about this
|
class |
StringMatcher
simple wrapper around Patter/Matcher pairs, with patterns using '*' wildcards
same as StringSetMatcher but for single patterns
|
class |
StringSetMatcher
simple utility that can be used to check for string matches in
sets with '*' wildcards, e.g.
|
class |
Trace<T>
a generic, listener- created trace over property specific operations
we could register this as a listener itself, but since it usually is used from
a listener, we might as well just delegate from there
|
class |
TraceElement<T>
encapsulates a listener-managed trace operation
|
class |
TypeRef
this is a utility construct for type references that should
not cause class loading when instantiated, but cannot use a
classname String because of argument type ambiguity (Strings are just
used everywhere).
|
class |
TypeSpec
wildcard supporting type specification to be used for JPF configuration.
|
class |
UnsortedArrayIntSet
a simplistic IntSet implementation that uses an unsorted array to keep elements.
|
class |
VarSpec
utility class to specify local variables in JPF options
example:
x.y.MyClass.foo(int,double):x
Note: this is not derived from FeatureSpec, it only used a MethodSpec for delegation
<2do> we don't deal with scopes or types yet
|
class |
WeakPool<E>
This is a simplified hash pool that does not support removal or
numbering of elements.
|
Modifier and Type | Field and Description |
---|---|
A |
Pair._1 |
B |
Pair._2 |
protected Object[] |
ObjVector.data
the backing array.
|
protected Object[] |
IdentityArrayObjectSet.elements |
Object[] |
SparseClusterArray.Chunk.elements |
static Object[] |
Misc.emptyObjectArray |
E |
ImmutableList.head |
E |
IntTable.Entry.key |
protected E[] |
IntTable.Snapshot.keys |
Modifier and Type | Method and Description |
---|---|
static Object |
ObjectList.add(Object head,
Object data) |
static <T> T[] |
Misc.appendArray(T[] base,
T... elements) |
static <T> T[] |
Misc.appendElement(T[] base,
T newElement) |
static <T> T[] |
Misc.arrayWithoutFirst(T[] base,
int nElements) |
Object |
CloneableObject.clone() |
static Object |
ObjectList.clone(Object head) |
static Object |
ObjectList.createList(Object... values)
this returns either the first value if there is only one element, or
a Node list containing all the values in the order they are provided
note - elements in the list occur in order of arguments, whereas normal
add() always adds at the head of the list
|
static Object |
ObjectList.forceSet(Object head,
Object newHead)
just to provide a way to overwrite SystemAttributes (e.g.
|
static Object |
ObjectList.get(Object head,
int idx) |
static <T> T[] |
Misc.getAddedElements(T[] oldArray,
T[] newArray) |
Object[] |
Invocation.getArguments() |
Object[] |
Invocation.getAttrs() |
Object[] |
Invocation.getExplicitArguments() |
static Object |
ObjectList.getFirst(Object head) |
static Object |
ObjectList.getNext(Object head,
Object prevData) |
static <T> T[] |
Misc.getRemovedElements(T[] oldArray,
T[] newArray) |
static Object |
ObjectConverter.javaObjectFromJPFObject(ElementInfo ei) |
static <T> T[] |
Misc.newArray(T... elements) |
Object |
ObjectList.Iterator.next() |
static <T> T[] |
Misc.prependArray(T[] base,
T... elements) |
static Object |
ObjectList.remove(Object head,
Object data) |
static <T> T[] |
Misc.removeElement(T[] base,
T element) |
static Object |
ObjectList.replace(Object head,
Object oldData,
Object newData) |
static Object |
ObjectList.set(Object head,
Object newHead) |
static <T> T[] |
Misc.stripNullElements(T[] oldArray) |
E[] |
ObjArray.toArray(E[] a) |
<F> F[] |
ObjVector.toArray(F[] dst) |
static Object |
ObjectList.valueOf(Object o) |
V[] |
PSIntMap.values() |
Modifier and Type | Method and Description |
---|---|
Iterator<Object> |
ObjectList.Iterator.iterator() |
Modifier and Type | Method and Description |
---|---|
void |
HashData.add(Object o) |
static Object |
ObjectList.add(Object head,
Object data) |
<F extends E> |
ObjVector.append(F[] x) |
<F extends E> |
ObjVector.append(F[] x,
int pos,
int len) |
static <T> T[] |
Misc.appendArray(T[] base,
T... elements) |
static <T> T[] |
Misc.appendArray(T[] base,
T... elements) |
static <T> T[] |
Misc.appendElement(T[] base,
T newElement) |
static <T> T[] |
Misc.arrayWithoutFirst(T[] base,
int nElements) |
static Object |
ObjectList.clone(Object head) |
static boolean |
Misc.compare(int len,
Object[] a1,
Object[] a2)
compare first len objects of two reference arrays, which can contain null
elements.
|
static boolean |
Misc.compare(int len,
Object[] a1,
Object[] a2)
compare first len objects of two reference arrays, which can contain null
elements.
|
static boolean |
Misc.compare(Object[] a1,
Object[] a2) |
static boolean |
Misc.compare(Object[] a1,
Object[] a2) |
void |
JPFLogger.config(Object... args) |
void |
JPFLogger.config(Object s1,
int s2) |
void |
JPFLogger.config(Object s1,
int s2,
Object s3,
int s4) |
void |
JPFLogger.config(Object s1,
Object s2) |
void |
JPFLogger.config(Object s1,
Object s2,
Object s3) |
void |
JPFLogger.config(Object s1,
Object s2,
Object s3,
Object s4) |
static boolean |
ObjectList.contains(Object head,
Object o) |
static <T> boolean |
Misc.contains(T[] array,
Object elem) |
static <T> boolean |
Misc.contains(T[] array,
Object elem) |
static boolean |
ObjectList.containsType(Object head,
Class<?> type) |
static <E> void |
ObjVector.copy(ObjVector<? extends E> src,
int srcPos,
E[] dst,
int dstPos,
int len) |
static Object |
ObjectList.createList(Object... values)
this returns either the first value if there is only one element, or
a Node list containing all the values in the order they are provided
note - elements in the list occur in order of arguments, whereas normal
add() always adds at the head of the list
|
static <T> T |
Misc.createObject(Class<T> cls,
Class<?>[] argTypes,
Object[] args) |
int |
ObjVector.dumpTo(Object[] dst,
int pos) |
void |
JPFLogger.entering(String sourceClass,
String sourceMethod,
Object param1) |
void |
JPFLogger.entering(String sourceClass,
String sourceMethod,
Object[] params) |
static boolean |
Misc.equal(Object a,
Object b) |
boolean |
BitSet64.equals(Object o) |
boolean |
IntArray.equals(Object o) |
boolean |
SourceRef.equals(Object o) |
boolean |
BitSet256.equals(Object o) |
boolean |
ArrayIntSet.equals(Object o) |
boolean |
Pair.equals(Object o) |
boolean |
BitArray.equals(Object o) |
boolean |
IntTable.Entry.equals(Object o) |
boolean |
ObjArray.equals(Object o) |
boolean |
FinalBitSet.equals(Object o) |
boolean |
Result.equals(Object o) |
boolean |
BitSet1024.equals(Object o) |
static boolean |
ObjectList.equals(Object head1,
Object head2) |
void |
JPFLogger.exiting(String sourceClass,
String sourceMethod,
Object result) |
void |
JPFLogger.ffine(String format,
Object... args) |
void |
JPFLogger.ffiner(String format,
Object... args) |
void |
JPFLogger.ffinest(String format,
Object... args) |
void |
JPFLogger.fine(Object... args) |
void |
JPFLogger.fine(Object s1,
int s2) |
void |
JPFLogger.fine(Object s1,
int s2,
Object s3,
int s4) |
void |
JPFLogger.fine(Object s1,
Object s2) |
void |
JPFLogger.fine(Object s1,
Object s2,
Object s3) |
void |
JPFLogger.fine(Object s1,
Object s2,
Object s3,
Object s4) |
void |
JPFLogger.finer(Object... args) |
void |
JPFLogger.finer(Object s1,
int s2) |
void |
JPFLogger.finer(Object s1,
int s2,
Object s3,
int s4) |
void |
JPFLogger.finer(Object s1,
Object s2) |
void |
JPFLogger.finer(Object s1,
Object s2,
Object s3) |
void |
JPFLogger.finer(Object s1,
Object s2,
Object s3,
Object s4) |
void |
JPFLogger.finest(Object... args) |
void |
JPFLogger.finest(Object s1,
int s2) |
void |
JPFLogger.finest(Object s1,
int s2,
Object s3,
int s4) |
void |
JPFLogger.finest(Object s1,
Object s2) |
void |
JPFLogger.finest(Object s1,
Object s2,
Object s3) |
void |
JPFLogger.finest(Object s1,
Object s2,
Object s3,
Object s4) |
void |
JPFLogger.finfo(String format,
Object... args) |
static Object |
ObjectList.forceSet(Object head,
Object newHead)
just to provide a way to overwrite SystemAttributes (e.g.
|
void |
JPFLogger.fsevere(String format,
Object... args) |
void |
JPFLogger.fwarning(String format,
Object... args) |
static Object |
ObjectList.get(Object head,
int idx) |
static <T> T[] |
Misc.getAddedElements(T[] oldArray,
T[] newArray) |
static <T> T[] |
Misc.getAddedElements(T[] oldArray,
T[] newArray) |
String |
Invocation.getArgumentValueLiteral(Object a) |
static Object |
ObjectList.getFirst(Object head) |
static <A> A |
ObjectList.getFirst(Object head,
Class<A> type) |
static <A> A |
ObjectList.getNext(Object head,
Class<A> type,
Object prevData) |
static Object |
ObjectList.getNext(Object head,
Object prevData) |
static <T,E> E |
Misc.getNextElementOfType(T[] base,
Class<E> elemType,
T prev) |
static <T> T[] |
Misc.getRemovedElements(T[] oldArray,
T[] newArray) |
static <T> T[] |
Misc.getRemovedElements(T[] oldArray,
T[] newArray) |
static <T> boolean |
Misc.hasElementOfType(T[] base,
Class<?> elemType) |
static void |
ObjectList.hash(Object head,
HashData hd) |
static int |
Misc.hashCode(Object o) |
static <T> int |
Misc.indexOf(T[] array,
Object elem) |
static <T> int |
Misc.indexOf(T[] array,
Object elem) |
void |
JPFLogger.info(Object... args) |
void |
JPFLogger.info(Object s1,
int s2) |
void |
JPFLogger.info(Object s1,
int s2,
Object s3,
int s4) |
void |
JPFLogger.info(Object s1,
Object s2) |
void |
JPFLogger.info(Object s1,
Object s2,
Object s3) |
void |
JPFLogger.info(Object s1,
Object s2,
Object s3,
Object s4) |
static boolean |
ObjectList.isEmpty(Object head) |
static boolean |
ObjectList.isList(Object head) |
static ObjectList.Iterator |
ObjectList.iterator(Object head) |
static int |
ObjectConverter.JPFObjectFromJavaObject(MJIEnv env,
Object javaObject)
Create JPF object from Java object
|
void |
JPFLogger.log(Level level,
String msg,
Object param1) |
void |
JPFLogger.log(Level level,
String msg,
Object[] params) |
void |
JPFLogger.logp(Level level,
String sourceClass,
String sourceMethod,
String msg,
Object param1) |
void |
JPFLogger.logp(Level level,
String sourceClass,
String sourceMethod,
String msg,
Object[] params) |
void |
JPFLogger.logrb(Level level,
String sourceClass,
String sourceMethod,
String bundleName,
String msg,
Object param1) |
void |
JPFLogger.logrb(Level level,
String sourceClass,
String sourceMethod,
String bundleName,
String msg,
Object[] params) |
boolean |
MethodSpec.matches(Object feature) |
boolean |
FieldSpec.matches(Object feature) |
boolean |
TypeSpec.matches(Object o) |
abstract boolean |
FeatureSpec.matches(Object feature) |
static <T> T[] |
Misc.newArray(T... elements) |
static int |
ObjectList.numberOfInstances(Object head,
Class<?> type) |
static <T> T[] |
Misc.prependArray(T[] base,
T... elements) |
static <T> T[] |
Misc.prependArray(T[] base,
T... elements) |
static void |
Debug.print(int l,
int k,
Object o) |
static void |
Debug.print(int l,
Object o) |
void |
ConsoleStream.print(Object o) |
static void |
Debug.println(int l,
int k,
Object o) |
static void |
Debug.println(int l,
Object o) |
void |
ConsoleStream.println(Object o) |
static Object |
ObjectList.remove(Object head,
Object data) |
static <T> T[] |
Misc.removeElement(T[] base,
T element) |
static Object |
ObjectList.replace(Object head,
Object oldData,
Object newData) |
static Object |
ObjectList.set(Object head,
Object newHead) |
void |
JPFLogger.severe(Object... args) |
void |
JPFLogger.severe(Object s1,
int s2) |
void |
JPFLogger.severe(Object s1,
int s2,
Object s3,
int s4) |
void |
JPFLogger.severe(Object s1,
Object s2) |
void |
JPFLogger.severe(Object s1,
Object s2,
Object s3) |
void |
JPFLogger.severe(Object s1,
Object s2,
Object s3,
Object s4) |
static int |
ObjectList.size(Object head) |
static <T> T[] |
Misc.stripNullElements(T[] oldArray) |
E[] |
ObjArray.toArray(E[] a) |
<F> F[] |
ObjVector.toArray(F[] dst) |
static String |
Misc.toString(Object[] array,
String prefix,
String separator,
String postfix) |
static <A> ObjectList.TypedIterator<A> |
ObjectList.typedIterator(Object head,
Class<A> type) |
static Object |
ObjectList.valueOf(Object o) |
void |
JPFLogger.warning(Object... args) |
void |
JPFLogger.warning(Object s1,
int s2) |
void |
JPFLogger.warning(Object s1,
int s2,
Object s3,
int s4) |
void |
JPFLogger.warning(Object s1,
Object s2) |
void |
JPFLogger.warning(Object s1,
Object s2,
Object s3) |
void |
JPFLogger.warning(Object s1,
Object s2,
Object s3,
Object s4) |
Constructor and Description |
---|
Invocation(MethodInfo mi,
Object[] args,
Object[] attrs) |
Invocation(MethodInfo mi,
Object[] args,
Object[] attrs) |
ObjArray(E[] data) |
ObjVector(F[] init) |
Modifier and Type | Class and Description |
---|---|
class |
Automaton<S extends State>
generic class for modeling automatons
Since this is used in so many extensions from both model and native code,
it seems appropriate to add a basis implementation to util.
|
class |
Transition |
Modifier and Type | Class and Description |
---|---|
class |
AbstractValue
Implementation of all Value methods.
|
class |
ArrayValue
Array parsed from JSON document
|
class |
CGCall |
class |
CGCreatorFactory
Singleton factory for creating CGCreators.
|
class |
CreatorsFactory |
class |
DoubleValue
Double value from JSON document
|
class |
JSONLexer
Lexical analyzer that reads stream and return JSON tokens.
|
class |
JSONObject
Object parsed from JSON document.
|
class |
JSONParser
JSON parser.
|
class |
StringValue
String value from JSON document
|
class |
Token
Token that is generated by JSONLexer.
|
Modifier and Type | Method and Description |
---|---|
boolean |
Token.equals(Object obj) |
Modifier and Type | Class and Description |
---|---|
class |
Alternative
ScriptElement that represents an alternative between choices.
|
class |
ESParser
generic parser for event scripts
<2do> this is still awfully hardwired to StringExpander
|
static class |
ESParser.DefaultEventFactory |
class |
ESParser.Exception
utilities
|
class |
Event |
class |
EventGenerator<T>
abstract ChoiceGenerator root for Event based generators
|
class |
EventGeneratorFactory
abstract root for backtrackable event generator factories
<2do> - we don't support backtracking for sections yet! needs to be implemented for
state charts
|
class |
Repetition |
class |
Script |
class |
ScriptElement |
class |
ScriptElementContainer |
protected class |
ScriptElementContainer.SECIterator |
class |
ScriptEnvironment<CG extends ChoiceGenerator<?>>
class representing a statemachine environment that produces SCEventGenerators
from scripts
|
class |
Section
this script element is just a way to do logical partitioning of scripts
and doesn't bear any additional info than just an id.
|
class |
SequenceInterpreter
an interpreter that walks a ScriptElementContainer hierarchy, returning
Events and Alternatives while expanding loops
|
class |
StringExpander
utility class to expand regular expression like strings.
|
class |
StringSetGenerator
that's mostly a test class to see what a script would be expanded to w/o
having any side effects in the ElementProcessor
|
Modifier and Type | Method and Description |
---|---|
Object |
SequenceInterpreter.clone() |
Object |
ScriptElementContainer.SECIterator.clone() |
static Object[][] |
Event.getBooleanArgVariations(int nArgs)
variations over boolean lists are quite easy to produce :)
|
Object[] |
Event.getConcreteArguments() |
Modifier and Type | Class and Description |
---|---|
class |
JPF_gov_nasa_jpf_util_test_TestJPF
native peer for our test class root
|
class |
JPF_gov_nasa_jpf_util_test_TestMultiProcessJPF |
class |
TestJPF
base class for JPF unit tests.
|
class |
TestMultiProcessJPF |
Modifier and Type | Method and Description |
---|---|
static void |
TestJPF.assertEquals(Object expected,
Object actual) |
static void |
TestJPF.assertEquals(String msg,
Object expected,
Object actual) |
static void |
TestJPF.assertNotNull(Object o) |
static void |
TestJPF.assertNotNull(String msg,
Object o) |
static void |
TestJPF.assertNull(Object o) |
static void |
TestJPF.assertNull(String msg,
Object o) |
static void |
TestJPF.assertSame(Object expected,
Object actual) |
static void |
TestJPF.assertSame(String msg,
Object expected,
Object actual) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractRestorer<Saved> |
class |
AbstractSerializer |
class |
Allocation
helper class for search global object id (SGOID) computation.
|
class |
AnnotationInfo
the JPF internal representation for Java Annotations
AnnotationInfos represent a separate type system.
|
static class |
AnnotationInfo.AnnotationAttribute |
static class |
AnnotationInfo.ClassValue |
static class |
AnnotationInfo.Entry |
static class |
AnnotationInfo.EnumValue |
class |
ApplicationContext
auxiliary class that captures the main entry and classloader context
of applications
|
class |
ArrayAccess
CG attribute to store array references of aload/astore operations
|
class |
ArrayFields
a Field (data value) store for array objects
|
class |
ArrayIndexOutOfBoundsExecutiveException |
class |
ArrayOffset
data encapsulation for backtracking.
|
class |
AtomicData
helper object to store per thread information about atomic line
execution
<2do> check if we can't do this less expensive.
|
class |
AtomicFieldUpdater
base class for atomic field updaters
NOTE - since all native methods are static, we have to be too
|
class |
BooleanArrayFields
element values for boolean[] objects
|
class |
BooleanChoiceGenerator
a pretty simple ChoiceGenerator that returns a boolean
there is not much use in having a CG type interface (such as
IntChoiceGenerator) since there is hardly a need for a generic type hierarchy
of BooleanChoiceGenerator subtypes - what else can you do with true/false
|
class |
BooleanFieldInfo
fieldinfo for slots holding booleans
|
class |
BoxObjectCacheManager |
class |
ByteArrayFields
element values for byte[] objects
|
class |
ByteFieldInfo
fieldinfo for slots holding bytes
|
class |
CharArrayFields
element values for char[] objects
|
class |
CharFieldInfo
fieldinfo for slots holding chars
|
class |
ChoiceGeneratorBase<T>
abstract root class for configurable choice generators
|
class |
ChoicePoint
a little helper class that is used to replay previously stored traces
(which are little more than just a list of ChoiceGenerator classnames and
choice indexes stored in a previous run)
|
class |
ClassFileContainer
abstract class that represents the source of a classfile, such
as (root) directories and jars
|
class |
ClassFileMatch
a lookup match for a given typename in a ClassFileContainer
|
class |
ClassInfo
Describes the VM's view of a java class.
|
class |
ClassInfoException |
class |
ClassLoaderInfo |
class |
ClassLoaderList
container for all ClassLoaderInfos that are in the current state.
|
class |
ClassParseException
an exception while parsing a ClassFile
|
class |
ClassPath
this is a lookup mechanism for class files that is based on an ordered
list of directory or jar entries
|
class |
ClinitRequired
this one is kind of a hack for situations where we detect deep from
the stack that we need a clinit to be executed, but we can't flag this
to the currently executed insn via a return value.
|
class |
ConfigAttributor
A configuration file-driven attributor so that we can tailor JPF's
attributor based on the application under test.
|
class |
ConstInsnPathTime
time model that uses instruction count along current path to deduce
the execution time.
|
class |
ContextBoundingSchedulerFactory
SchedulerFactory that limits the search by imposing a maximum number of
thread preemptions (i.e., preempting context switches) that can occur per execution
path.
|
class |
DebugJenkinsStateSet
a JenkinsStateSet that stores program state information in a readable
and diffable format.
|
class |
DefaultAttributor
default Attributor implementation to set method and fiel attributes
at class load time.
|
class |
DefaultBacktracker<KState> |
class |
DefaultFieldsFactory
our concrete Fields factory (representing the default JPF object model)
|
class |
DefaultMementoRestorer
a MementoRestorer that uses the default mementos
|
class |
DefaultSchedulerFactory
the general policy is that we only create Thread CGs here (based on their
status), but we don't change any thread or lock status.
|
class |
DirectCallStackFrame
DirectCallStackFrames are only used for overlay calls (from native code), i.e.
|
class |
DistributedSchedulerFactory |
class |
DoubleArrayFields
element values for double[] objects
|
class |
DoubleFieldInfo
type, name and attribute information for 'double' fields
|
class |
DoubleSlotFieldInfo
a double or long field
|
class |
DynamicElementInfo
A specialized version of ElementInfo that represents heap objects
|
class |
ElementInfo
Describes an element of memory containing the field values of a class or an
object.
|
class |
ExceptionHandler
Stores the information about an exception handler.
|
class |
ExceptionInfo
helper class to store context of an exception
|
class |
FieldInfo
type, name and attribute information of a field.
|
class |
FieldLockInfo
class encapsulating the lock protection status for field access
instructions.
|
class |
Fields
Represents the variable, hash-collapsed pooled data associated with an object
that is related to the object values (as opposed to synchronization ->Monitor).
|
class |
FloatArrayFields
element values for float[] objects
|
class |
FloatFieldInfo
type, name, modifier info of float fields
|
class |
FullStateSet
Implements a lossless StateSet
|
class |
GenericHeap
this is an abstract root for Heap implementations, providing a standard
mark&sweep collector, change attribute management, and generic pinDownList,
weakReference and internString handling
The concrete Heap implementors have to provide the ElementInfo collection
and associated getters, allocators and iterators
|
protected class |
GenericHeap.ElementInfoMarker |
class |
GenericSGOIDHeap
abstract Heap trait that implements SGOIDs by means of a search global
Allocation map and a state managed allocCount map
|
class |
GlobalTrackingPolicy
a SharedObjectPolicy that uses search global ThreadInfoSets, i.e.
|
class |
HandlerContext
utility wrapper for exception handlers that /would/ handle
a given exception type
<2do> This should be a class hierarchy to properly distinguish between
ordinary catch handlers and UncaughtHandler objects, but so far
this isn't worth it
|
class |
HashedAllocationContext
an AllocationContext that uses a hash value for comparison.
|
class |
InfoObject
common root for ClassInfo, MethodInfo, FieldInfo (and maybe more to follow)
so far, it's used to factorize the annotation support, but we can also
move the attributes up here
|
class |
Instruction
common root of all JPF bytecode instruction classes
|
class |
IntArrayFields
element values for int[] objects
|
class |
IntegerFieldInfo
type, name, mod info about integer fields
|
class |
JenkinsStateSet
Implements StateSet based on Jenkins hashes.
|
class |
JPF_gov_nasa_jpf_AnnotationProxyBase
native peer for Annotation Proxies
(saves us some bytecode interpretation shoe leather)
|
class |
JPF_gov_nasa_jpf_CachedROHttpConnection
very simple URLConnection model that can be used for reading static URL contents
The data can be stored in/read from the file system, and is cached
to avoid DOS by means of model checking
|
class |
JPF_gov_nasa_jpf_ConsoleOutputStream
MJI NativePeer class to intercept all System.out and System.err
printing.
|
class |
JPF_gov_nasa_jpf_DelegatingTimeZone
native peer for JPFs concrete TimeZone class, which is just delegating to the
host VM so that we are independent of Java versions
|
class |
JPF_gov_nasa_jpf_SerializationConstructor |
class |
JPF_gov_nasa_jpf_test_MemoryGoal
native peer for MemoryGoal tests
|
class |
JPF_gov_nasa_jpf_tools_MethodTester
native peer for the MethodTester tool
|
class |
JPF_gov_nasa_jpf_vm_Verify
native peer class for programmatic JPF interface (that can be used inside
of apps to verify - if you are aware of the danger that comes with it)
this peer is a bit different in that it only uses static fields and methods because
its use is supposed to be JPF global (without classloader namespaces)
|
class |
JPF_java_io_File
intercept and forward some of the filesystem access methods.
|
class |
JPF_java_io_FileDescriptor
native peer for file descriptors, which are our basic interface to
access file contents.
|
class |
JPF_java_io_InputStreamReader |
class |
JPF_java_io_ObjectInputStream |
class |
JPF_java_io_ObjectOutputStream |
class |
JPF_java_io_ObjectStreamClass |
class |
JPF_java_io_OutputStreamWriter
native peer for OutputStreamWriter, to avoid that we have the
char-to-byte conversion in JPF
<2do> this needs to be de-staticed (see model class)
|
class |
JPF_java_io_RandomAccessFile
MJI NativePeer class for java.io.RandomAccessFile library abstraction
|
class |
JPF_java_lang_Boolean |
class |
JPF_java_lang_Byte |
class |
JPF_java_lang_Character
MJI NativePeer class for java.lang.Character library abstraction
Whoever is using this seriously is definitely screwed, performance-wise
|
class |
JPF_java_lang_Class
MJI NativePeer class for java.lang.Class library abstraction
|
class |
JPF_java_lang_ClassLoader |
class |
JPF_java_lang_Double
MJI NativePeer class for java.lang.Double library abstraction
|
class |
JPF_java_lang_Float
MJI NativePeer class for java.lang.Float library abstraction
|
class |
JPF_java_lang_Integer
MJI NativePeer class for java.lang.Integer library abstraction
|
class |
JPF_java_lang_Long
MJI NativePeer class for java.lang.Long library abstraction
|
class |
JPF_java_lang_Math
MJI NativePeer class for java.lang.Math library abstraction
|
class |
JPF_java_lang_Object
MJI NativePeer class for java.lang.Object library abstraction
|
class |
JPF_java_lang_reflect_Array
MJI NativePeer class for java.lang.reflect.Array library abstraction
|
class |
JPF_java_lang_reflect_Constructor
native peer for rudimentary constructor reflection.
|
class |
JPF_java_lang_reflect_Field |
class |
JPF_java_lang_reflect_Method |
class |
JPF_java_lang_reflect_Proxy |
class |
JPF_java_lang_Runtime
just a dummy for now, to avoid UnsatisfiedLinkErrors
|
class |
JPF_java_lang_Short
MJI NativePeer class for java.lang.Short library abstraction
|
class |
JPF_java_lang_String
MJI NativePeer class for java.lang.String library abstraction
|
class |
JPF_java_lang_StringBuffer
MJI NativePeer class for java.lang.StringBuffer library abstraction
|
class |
JPF_java_lang_StringBuilder |
class |
JPF_java_lang_StringCoding
we are not really interested in model checking this, so we intercept
and ignore
<2do> at some point we should probably do proper decoding/encoding,
but the java.lang.StringCoding class is unfortunately not public,
and it would be a pain to work around the access restrictions
|
class |
JPF_java_lang_System
MJI NativePeer class for java.lang.System library abstraction
|
class |
JPF_java_lang_Thread
MJI NativePeer class for java.lang.Thread library abstraction
NOTE - this implementation depends on all live thread objects being
in ThreadList
|
class |
JPF_java_lang_Throwable
MJI NativePeer class for java.lang.Throwable library abstraction
|
class |
JPF_java_net_URLClassLoader |
class |
JPF_java_net_URLDecoder
native peer for java.net.URLDecoder forwarding
|
class |
JPF_java_net_URLEncoder
native peer for java.net.URLEncoder forwarding
|
class |
JPF_java_security_MessageDigest |
class |
JPF_java_text_Bidi |
class |
JPF_java_text_DateFormat
this is just the minimal support for DateFormat.parse(String)
|
class |
JPF_java_text_DateFormatSymbols |
class |
JPF_java_text_DecimalFormat |
class |
JPF_java_text_DecimalFormatSymbols
MJI NativePeer class for java.text.DecimalFormatSymbols library abstraction
we need to intercept the initialization because it is requires
file io (properties) based on the Locale
|
class |
JPF_java_text_Format
native peer for java.text.Format delegation.
|
class |
JPF_java_text_SimpleDateFormat
(incomplete) native peer for SimpleDateFormat.
|
class |
JPF_java_util_Calendar |
class |
JPF_java_util_concurrent_atomic_AtomicInteger
native peer for java.util.concurrent.atomic.AtomicInteger
this implementation just cuts off native methods
|
class |
JPF_java_util_concurrent_atomic_AtomicIntegerArray
native peer for java.util.concurrent.atomic.AtomicIntegerArray
|
class |
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater
a full peer for the AtomicIntegerFieldUpdater
|
class |
JPF_java_util_concurrent_atomic_AtomicLong
native peer for java.util.concurrent.atomic.AtomicLong
this implementation just cuts off native methods
|
class |
JPF_java_util_concurrent_atomic_AtomicLongArray
native peer for java.util.concurrent.atomic.AtomicLongArray
|
class |
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater
a full peer for the AtomicLongFieldUpdater
|
class |
JPF_java_util_concurrent_atomic_AtomicReferenceArray
native peer for java.util.concurrent.atomic.AtomicReferenceArray
|
class |
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater
a full peer for the AtomicReferenceFieldUpdater
|
class |
JPF_java_util_Date |
class |
JPF_java_util_Locale |
class |
JPF_java_util_logging_Level
this is only a skeleton to make basic logging work under JPF
|
class |
JPF_java_util_Random
MJI NativePeer class for java.util.Random library abstraction
model - peer delegation is done via restoring a singleton, which unfortunately
has to resort to the rather nasty Unsafe mechanism because the required
random internals are private.
|
class |
JPF_java_util_regex_Matcher
native peer for a regex Matcher
this is just a delegatee peer
|
class |
JPF_java_util_regex_Pattern |
class |
JPF_java_util_ResourceBundle
native peer for ResourceBundle
|
class |
JPF_java_util_TimeZone
native peer for java.util.TimeZone
this is a (mostly) delegating implementation that became necessary because TimeZone has been
considerably changed in Java 1.7 (OpenJDK) and we need a version that is compatible with
pre and post 1.7 releases
|
class |
JPF_sun_misc_Hashing
simple forwarding sun.misc.Hashing peer to speed up execution and shorten traces
|
class |
JPF_sun_misc_Unsafe
we don't want this class! This is a hodgepodge of stuff that shouldn't be in Java, but
is handy for some hacks.
|
class |
JPF_sun_misc_VM
this is just a placeholder for now, we don't support its functionality
|
class |
JPF_sun_net_www_protocol_http_Handler
native peer to configure concrete URLConnection classes for specific URLs
We use model class configuration in case somebody wants to implement logic
in there that requires backtracking, and doesn't want to do this on the
native peer level
example config:
http.connection= http://*.dtd => gov.nasa.jpf.CachedROHttpConnection, http://foo.com/* -- x.y.MyHttpConnection
|
class |
JPF_sun_reflect_Reflection |
class |
JPF_sun_reflect_ReflectionFactory
<2do> hack around a hack - we need to override this as long as we don't
replace ObjectStreamClass
|
class |
JPFOutputStream
stream to write program state info in a readable and diff-able format.
|
class |
KernelState
This class represents the SUT program state (statics, heap and threads)
|
class |
LoadOnJPFRequired |
class |
LocalVarInfo |
class |
LongArrayFields
element values for long[] objects
|
class |
LongFieldInfo |
class |
MementoRestorer
state storer/restorer that works solely on a snapshot basis
|
class |
MethodInfo
information associated with a method.
|
class |
MJIEnv
MJIEnv is the call environment for "native" methods, i.e.
|
class |
Monitor
Represents the variable, hash-collapsed pooled data associated with an object
that is not related to the object values (->Fields), but to the use of the
object for synchronization purposes (locks and signals).
|
class |
MultiProcessVM
A VM implementation that simulates running multiple applications within the same
JPF process (centralized model checking of distributed applications).
|
class |
NamedFields
value container for non-array classes
|
class |
NativeMethodInfo
a MethodInfo for a native peer executed method
|
class |
NativePeer
native peer classes are part of MJI and contain the code that is
executed by the host VM (i.e.
|
class |
NativeStackFrame
a stack frame for MJI methods
This is a special Stackframe to execute NativeMethodInfos, which are just a wrapper around Java reflection
calls.
|
class |
NoOutOfMemoryErrorProperty
A property class so that gov.nasa.jpf.JPF can add an error to the
gov.nasa.jpf.search.Search object when JPF catches an OutOfMemoryError.
|
class |
NotDeadlockedProperty
property class to check for no-runnable-threads conditions
|
class |
NoUncaughtExceptionsProperty
property class to check for uncaught exceptions
|
class |
ObjRef
helper class to store object references in a context where Integer is used for boxed 'int' values
|
class |
OverlappingContenderPolicy
a thread tracking policy that uses ThreadInfoSets which are
search global from the point of object creation.
|
class |
OVHeap
a heap that implements search global object ids (SGOIDs) and uses
a simple ObjVector to store ElementInfos.
|
class |
OVStatics
Statics implementation that uses a simple ObjVector as the underlying container.
|
class |
Path
Path represents the data structure in which a execution trace is recorded.
|
class |
PreciseAllocationContext
class that captures execution context consisting of executing thread and
pc's of ti's current StackFrames
note that we pool (i.e.
|
class |
PredicateMap |
class |
PrioritySchedulerFactory
a scheduler policy which always runs one of the threads that
have equal top priority
|
class |
PSIMHeap
heap implementation that uses a PersistentStagingMsbIntMap as the underlying container
This is intended for large state spaces, to minimize store/restore costs.
|
class |
ReferenceArrayFields
element values for reference array objects
(references are stored as int's)
|
class |
ReferenceFieldInfo
field info for object fields
|
class |
RestorableVMState
NOTE - making VMStates fully restorable is currently very
expensive and should only be done on a selective basis
|
class |
SerializingStateSet |
class |
SharedObjectPolicy
abstraction for configured policy object that is responsible for detecting shared objects and classes
The interface has to support both
tracking (actual access) based policies
("what is shared")
conservative reachability based policies
("what could be shared")
The interface is intentionally kept generic to support both policies since tracking - while being
far more efficient in terms of states and speed - can either miss some paths or cause state spaces
to depend on search history, thus leading to different search graphs for randomized searches.
|
class |
ShortArrayFields
element values for short[] objects
|
class |
ShortFieldInfo
fieldinfo for slots holding booleans
|
class |
SingleProcessVM |
class |
SingleSlotFieldInfo
field type that requires a single slot (all but long and double)
|
class |
StackFrame
Describes callerSlots stack frame.
|
class |
StaticElementInfo
A specialized version of ElementInfo that is used for static fields.
|
class |
StatisticFieldLockInfoFactory
a FieldLockInfo implementation with the following strategy:
- at each check, store the intersection of the current threads lock set
with the previous field lock set
- if the access was checked less than CHECK_THRESHOLD times, report the
field as unprotected
- if the field lock set doesn't become empty after CHECK_THRESHOLD, report
the field as protected
- as an optimization, raise the check level above the threshold if we
have a good probability that a current lock is a protection lock for this
field
- continue to check even after reaching the threshold, so that we
can at least report a violated assumption
NOTE there is a subtle problem: if we ever falsely assume lock protection
in a path that subsequently recycles the shared object (e.g.
|
class |
Step
this corresponds to an executed instruction.
|
class |
SystemClassLoaderInfo |
class |
SystemState
the class that encapsulates not only the current execution state of the VM
(the KernelState), but also the part of it's history that is required
by VM to backtrack, plus some potential annotations that can be used to
control the search (i.e.
|
class |
SystemTime
simple delegating TimeModel implementation that just returns System time.
|
class |
ThreadData
this is the mutable Thread data we have to keep track of for storing/restoring states
|
class |
ThreadInfo
Represents a thread.
|
protected class |
ThreadInfo.InvokedStackIterator |
protected class |
ThreadInfo.StackIterator |
class |
ThreadList
Contains the list of all ThreadInfos for live java.lang.Thread objects
We add a thread upon creation (within the ThreadInfo ctor), and remove it
when the corresponding java.lang.Thread object gets recycled by JPF.
|
static class |
ThreadList.Count |
class |
TidSet
set that stores threads via (search global) thread ids.
|
class |
Transition.StepIterator |
class |
Types
various type mangling/demangling routines
This reflects the general type id mess in Java.
|
class |
UncaughtException
represents the case of an unhandled exception detected by JPF
This is a "controlflow exception", but I finally made my peace with it since
UncaughtExceptions can be thrown from various places, including the VM (
|
class |
Verify
Verify is the programmatic interface of JPF that can be used from inside of
applications.
|
class |
VM
This class represents the virtual machine.
|
Modifier and Type | Field and Description |
---|---|
protected Object |
InfoObject.attr
user defined attribute objects.
|
protected Object |
ChoiceGeneratorBase.attr |
protected Object |
Instruction.attr |
protected Object[] |
StackFrame.attrs |
protected Saved |
AbstractRestorer.cached |
protected Object |
FieldInfo.cv |
protected Object[] |
Fields.fieldAttrs
we use this to store arbitrary field attributes (like symbolic values),
but only pushClinit this on demand
|
protected Object |
StackFrame.frameAttr |
protected Object |
Fields.objectAttr
attribute attached to the object as a whole
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<Object> |
DefaultBacktracker.sstack
and that adds the SystemState specifics
|
Modifier and Type | Method and Description |
---|---|
Object |
DynamicElementInfo.asBoxObject() |
Object |
ElementInfo.asBoxObject() |
Object |
ThreadInfo.clone() |
Object |
ThreadList.clone() |
Object |
MethodInfo.clone() |
Object |
AtomicData.clone() |
Object |
FieldLockInfo.clone() |
Object |
Transition.clone() |
Object |
Transition.getAnnotation() |
Object[] |
MJIEnv.getArgAttributes()
return attr list of all arguments.
|
Object[] |
MJIEnv.getArgumentArray(int argRef) |
Object[] |
StackFrame.getArgumentAttrs(MethodInfo miCallee)
return an array of all argument attrs, which in turn can be lists.
|
Object[] |
NativeStackFrame.getArguments() |
protected Object[] |
NativeMethodInfo.getArguments(ThreadInfo ti)
Get and convert the native method parameters off the ThreadInfo stack.
|
Object |
InfoObject.getAttr()
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
ChoiceGeneratorBase.getAttr()
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
ChoiceGenerator.getAttr()
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
Instruction.getAttr()
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
ElementInfo.getBacktrackData() |
Object |
SystemState.getBacktrackData() |
static Object |
AnnotationInfo.getClassValue(String type) |
Object |
FieldInfo.getConstantValue() |
Object |
StackFrame.getDoubleResultAttr() |
Object |
ElementInfo.getElementAttr(int idx)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
MJIEnv.getElementAttr(int objref,
int idx)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
static Object |
AnnotationInfo.getEnumValue(String eType,
String eConst) |
Object |
ElementInfo.getFieldAttr(FieldInfo fi)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
Fields.getFieldAttr(int fieldOrElementIndex)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
MJIEnv.getFieldAttr(int objref,
String fname)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
StackFrame.getFieldValue(String id) |
Object |
ElementInfo.getFieldValueObject(String fname) |
Object |
StackFrame.getFloatResultAttr() |
Object |
StackFrame.getFrameAttr()
this returns all of them - use either if you know there will be only
one attribute at callerSlots time, or check/process result with ObjectList
|
Object |
StackFrame.getLocalAttr(int index)
this returns all of them - use either if you know there will be only
one attribute at callerSlots time, or check/process result with ObjectList
|
Object |
StackFrame.getLocalOrFieldValue(String id) |
Object |
StackFrame.getLocalValueObject(LocalVarInfo lv) |
Object |
StackFrame.getLongOperandAttr()
this returns all of them - use either if you know there will be only
one attribute at callerSlots time, or check/process result with ObjectList
|
Object |
NativeStackFrame.getLongResultAttr() |
abstract Object |
StackFrame.getLongResultAttr() |
static Object |
Verify.getObject(String key) |
Object |
ElementInfo.getObjectAttr()
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
Fields.getObjectAttr()
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
MJIEnv.getObjectAttr(int objref)
this returns all of them - use either if you know there will be only
one attribute at a time, or check/process result with ObjectList
|
Object |
StackFrame.getOperandAttr()
this returns all of them - use either if you know there will be only
one attribute at callerSlots time, or check/process result with ObjectList
|
Object |
StackFrame.getOperandAttr(int offset)
this returns all of them - use either if you know there will be only
one attribute at callerSlots time, or check/process result with ObjectList
|
Object |
SystemState.getRestoreData() |
Object |
NativeStackFrame.getResultAttr() |
abstract Object |
StackFrame.getResultAttr() |
Object |
NativeStackFrame.getReturnAttr() |
Object |
MJIEnv.getReturnAttribute() |
Object |
NativeStackFrame.getReturnValue() |
Object |
StackFrame.getSlotAttr(int i) |
Object[] |
StackFrame.getSlotAttrs() |
Object |
ClassInfo.getStaticFieldValueObject(String id) |
Object |
AnnotationInfo.Entry.getValue() |
Object |
AnnotationInfo.getValue(String key)
this is the common getter that should trigger parsing the corresponding class file
|
abstract Object |
FieldInfo.getValueObject(Fields data) |
Object |
BooleanFieldInfo.getValueObject(Fields f) |
Object |
IntegerFieldInfo.getValueObject(Fields f) |
Object |
FloatFieldInfo.getValueObject(Fields f) |
Object |
ShortFieldInfo.getValueObject(Fields f) |
Object |
ByteFieldInfo.getValueObject(Fields f) |
Object |
DoubleFieldInfo.getValueObject(Fields f) |
Object |
ReferenceFieldInfo.getValueObject(Fields f) |
Object |
CharFieldInfo.getValueObject(Fields f) |
Object |
LongFieldInfo.getValueObject(Fields f) |
Object |
IntArrayFields.getValues() |
Object |
FloatArrayFields.getValues() |
Object |
ReferenceArrayFields.getValues() |
abstract Object |
ArrayFields.getValues() |
Object |
ByteArrayFields.getValues() |
Object |
DoubleArrayFields.getValues() |
Object |
BooleanArrayFields.getValues() |
Object |
CharArrayFields.getValues() |
Object |
ShortArrayFields.getValues() |
Object |
LongArrayFields.getValues() |
static Object |
Verify.randomObject(String type) |
Object |
AnnotationInfo.value() |
Modifier and Type | Method and Description |
---|---|
void |
InfoObject.addAttr(Object a) |
void |
ChoiceGeneratorBase.addAttr(Object a) |
void |
ChoiceGenerator.addAttr(Object a) |
void |
Instruction.addAttr(Object a) |
void |
MJIEnv.addElementAttr(int objref,
int idx,
Object a) |
void |
ElementInfo.addElementAttr(int idx,
Object a) |
static void |
Verify.addElementAttribute(Object arr,
int idx,
int val) |
void |
ElementInfo.addElementAttrNoClone(int idx,
Object a)
<2do> those will be obsolete
|
void |
ElementInfo.addFieldAttr(FieldInfo fi,
Object a) |
void |
Fields.addFieldAttr(int nFieldsOrElements,
int fieldOrElementIndex,
Object attr) |
void |
MJIEnv.addFieldAttr(int objref,
String fname,
Object a) |
static void |
Verify.addFieldAttribute(Object o,
String fieldName,
int val) |
void |
StackFrame.addFrameAttr(Object attr) |
void |
StackFrame.addLocalAttr(int index,
Object attr) |
void |
StackFrame.addLongOperandAttr(Object a) |
void |
MJIEnv.addObjectAttr(int objref,
Object a) |
void |
ElementInfo.addObjectAttr(Object a) |
void |
Fields.addObjectAttr(Object attr) |
static void |
Verify.addObjectAttribute(Object o,
int val) |
void |
StackFrame.addOperandAttr(int offset,
Object a) |
void |
StackFrame.addOperandAttr(Object a) |
void |
SystemState.backtrackTo(Object backtrackData) |
boolean |
IntArrayFields.equals(Object o) |
boolean |
FloatArrayFields.equals(Object o) |
boolean |
ClassInfo.equals(Object o) |
boolean |
ObjRef.equals(Object o) |
boolean |
StaticElementInfo.equals(Object o) |
boolean |
ReferenceArrayFields.equals(Object o) |
boolean |
Allocation.equals(Object o) |
boolean |
NativeStackFrame.equals(Object object) |
boolean |
ByteArrayFields.equals(Object o) |
boolean |
ElementInfo.equals(Object o) |
boolean |
NamedFields.equals(Object o)
Checks for equality.
|
boolean |
AtomicData.equals(Object o) |
boolean |
DoubleArrayFields.equals(Object o) |
abstract boolean |
Fields.equals(Object o) |
boolean |
BooleanArrayFields.equals(Object o)
we check for type and equal element values
|
boolean |
HashedAllocationContext.equals(Object o) |
boolean |
CharArrayFields.equals(Object o) |
boolean |
Monitor.equals(Object o)
Compares to another object.
|
boolean |
ShortArrayFields.equals(Object o) |
boolean |
ThreadData.equals(Object o) |
boolean |
StackFrame.equals(Object o) |
boolean |
PreciseAllocationContext.equals(Object o) |
boolean |
LongArrayFields.equals(Object o) |
static void |
Verify.freezeSharedness(Object o,
boolean freeze) |
static int |
Verify.getElementAttribute(Object arr,
int idx) |
static int[] |
Verify.getElementAttributes(Object arr,
int idx) |
static int |
Verify.getFieldAttribute(Object o,
String fieldName) |
static int[] |
Verify.getFieldAttributes(Object o,
String fieldName) |
static <T> T |
NativePeer.getInstance(Class<?> cls,
Class<T> type,
Class<?>[] argTypes,
Object[] args) |
<A> A |
ChoiceGenerator.getNextAttr(Class<A> attrType,
Object prev) |
<T> T |
InfoObject.getNextAttr(Class<T> attrType,
Object prev) |
<T> T |
ChoiceGeneratorBase.getNextAttr(Class<T> attrType,
Object prev) |
<T> T |
Instruction.getNextAttr(Class<T> attrType,
Object prev) |
<T> T |
ElementInfo.getNextElementAttr(int idx,
Class<T> attrType,
Object prev) |
<T> T |
ElementInfo.getNextFieldAttr(FieldInfo fi,
Class<T> attrType,
Object prev) |
<T> T |
Fields.getNextFieldAttr(int fieldOrElementIndex,
Class<T> type,
Object prev) |
<T> T |
StackFrame.getNextFrameAttr(Class<T> attrType,
Object prev) |
<T> T |
StackFrame.getNextLocalAttr(int index,
Class<T> attrType,
Object prev) |
<T> T |
StackFrame.getNextLongOperandAttr(Class<T> attrType,
Object prev) |
<T> T |
ElementInfo.getNextObjectAttr(Class<T> attrType,
Object prev) |
<T> T |
Fields.getNextObjectAttr(Class<T> attrType,
Object prev) |
<T> T |
StackFrame.getNextOperandAttr(Class<T> attrType,
Object prev) |
<T> T |
StackFrame.getNextOperandAttr(int offset,
Class<T> attrType,
Object prev) |
static int |
Verify.getObjectAttribute(Object o) |
static int[] |
Verify.getObjectAttributes(Object o) |
ClosedMemento |
SystemState.getRestorer(Object key) |
boolean |
InfoObject.hasAttrValue(Object a) |
boolean |
ChoiceGeneratorBase.hasAttrValue(Object a) |
boolean |
StackFrame.hasFrameAttrValue(Object a) |
boolean |
SystemState.hasRestorer(Object key) |
static boolean |
Verify.isShared(Object o) |
static void |
Verify.log(String loggerId,
int logLevel,
String format,
Object... args) |
void |
SystemState.putRestorer(Object key,
ClosedMemento restorer)
call the provided restorer each time we get back to this state
|
void |
InfoObject.removeAttr(Object a) |
void |
ChoiceGeneratorBase.removeAttr(Object a) |
void |
ChoiceGenerator.removeAttr(Object a) |
void |
Instruction.removeAttr(Object a) |
void |
ElementInfo.removeElementAttr(int idx,
Object a) |
void |
ElementInfo.removeElementAttrNoClone(int idx,
Object a) |
void |
ElementInfo.removeFieldAttr(FieldInfo fi,
Object a) |
void |
Fields.removeFieldAttr(int fieldOrElementIndex,
Object attr) |
void |
StackFrame.removeFrameAttr(Object attr) |
void |
StackFrame.removeLocalAttr(int index,
Object attr) |
void |
StackFrame.removeLongOperandAttr(Object a) |
void |
ElementInfo.removeObjectAttr(Object a) |
void |
Fields.removeObjectAttr(Object attr) |
void |
StackFrame.removeOperandAttr(int offset,
Object a) |
void |
StackFrame.removeOperandAttr(Object a) |
void |
InfoObject.replaceAttr(Object oldAttr,
Object newAttr) |
void |
ChoiceGeneratorBase.replaceAttr(Object oldAttr,
Object newAttr) |
void |
ChoiceGenerator.replaceAttr(Object oldAttr,
Object newAttr) |
void |
Instruction.replaceAttr(Object oldAttr,
Object newAttr) |
void |
ElementInfo.replaceElementAttr(int idx,
Object oldAttr,
Object newAttr) |
void |
ElementInfo.replaceElementAttrNoClone(int idx,
Object oldAttr,
Object newAttr) |
void |
ElementInfo.replaceFieldAttr(FieldInfo fi,
Object oldAttr,
Object newAttr) |
void |
Fields.replaceFieldAttr(int fieldOrElementIndex,
Object oldAttr,
Object newAttr) |
void |
StackFrame.replaceFrameAttr(Object oldAttr,
Object newAttr) |
void |
StackFrame.replaceLocalAttr(int index,
Object oldAttr,
Object newAttr) |
void |
StackFrame.replaceLongOperandAttr(Object oldAttr,
Object newAttr) |
void |
ElementInfo.replaceObjectAttr(Object oldAttr,
Object newAttr) |
void |
Fields.replaceObjectAttr(Object oldAttr,
Object newAttr) |
void |
StackFrame.replaceOperandAttr(int offset,
Object oldAttr,
Object newAttr) |
void |
StackFrame.replaceOperandAttr(Object oldAttr,
Object newAttr) |
void |
SystemState.restoreTo(Object backtrackData) |
void |
Transition.setAnnotation(Object o) |
void |
NativeStackFrame.setArgs(Object[] args) |
abstract void |
DirectCallStackFrame.setArgument(int idx,
int value,
Object attr) |
void |
NativeStackFrame.setArgumentLocal(int idx,
int value,
Object attr) |
abstract void |
StackFrame.setArgumentLocal(int idx,
int value,
Object attr) |
void |
InfoObject.setAttr(Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
ChoiceGeneratorBase.setAttr(Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
ChoiceGenerator.setAttr(Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
Instruction.setAttr(Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
AnnotationInfo.setClonedEntryValue(String key,
Object newValue) |
void |
FieldInfo.setConstantValue(Object constValue) |
void |
BooleanFieldInfo.setConstantValue(Object constValue) |
void |
IntegerFieldInfo.setConstantValue(Object constValue) |
void |
FloatFieldInfo.setConstantValue(Object constValue) |
void |
ShortFieldInfo.setConstantValue(Object constValue) |
void |
ByteFieldInfo.setConstantValue(Object constValue) |
void |
DoubleFieldInfo.setConstantValue(Object constValue) |
void |
ReferenceFieldInfo.setConstantValue(Object constValue) |
void |
CharFieldInfo.setConstantValue(Object constValue) |
void |
LongFieldInfo.setConstantValue(Object constValue) |
void |
DirectCallStackFrame.setDoubleArgument(int idx,
double value,
Object attr) |
void |
StackFrame.setDoubleArgumentLocal(int idx,
double value,
Object attr) |
void |
MJIEnv.setElementAttr(int objref,
int idx,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
ElementInfo.setElementAttr(int idx,
Object attr)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
static void |
Verify.setElementAttribute(Object arr,
int idx,
int val) |
void |
ElementInfo.setElementAttrNoClone(int idx,
Object attr)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
ElementInfo.setFieldAttr(FieldInfo fi,
Object attr)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
Fields.setFieldAttr(int nFieldsOrElements,
int fieldOrElementIndex,
Object attr)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
MJIEnv.setFieldAttr(int objref,
String fname,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
static void |
Verify.setFieldAttribute(Object o,
String fieldName,
int val)
note - these are mostly for debugging purposes (to see if attributes get
propagated correctly, w/o having to write a listener), since attributes are
supposed to be created at the native side, and hence can't be accessed from
the application
|
void |
DirectCallStackFrame.setFloatArgument(int idx,
float value,
Object attr) |
void |
StackFrame.setFloatArgumentLocal(int idx,
float value,
Object attr) |
void |
StackFrame.setFrameAttr(Object attr)
this replaces all of them - use only if you know there are no
SystemAttributes in the list (which would cause an exception)
|
void |
StackFrame.setLocalAttr(int index,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at callerSlots time
- you obtained the value you set by callerSlots previous getXAttr()
- you constructed callerSlots multi value list with ObjectList.createList()
|
abstract void |
DirectCallStackFrame.setLongArgument(int idx,
long value,
Object attr) |
void |
NativeStackFrame.setLongArgumentLocal(int idx,
long value,
Object attr) |
abstract void |
StackFrame.setLongArgumentLocal(int idx,
long value,
Object attr) |
void |
StackFrame.setLongOperandAttr(Object a)
this replaces all of them - use only if you know
- there will be only one attribute at callerSlots time
- you obtained the value you set by callerSlots previous getXAttr()
- you constructed callerSlots multi value list with ObjectList.createList()
|
void |
MJIEnv.setObjectAttr(int objref,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
ElementInfo.setObjectAttr(Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
Fields.setObjectAttr(Object attr)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
static void |
Verify.setObjectAttribute(Object o,
int val) |
void |
ElementInfo.setObjectAttrNoClone(Object a)
this replaces all of them - use only if you know
- there will be only one attribute at a time
- you obtained the value you set by a previous getXAttr()
- you constructed a multi value list with ObjectList.createList()
|
void |
StackFrame.setOperandAttr(int offset,
Object a)
this replaces all of them - use only if you know
- there will be only one attribute at callerSlots time
- you obtained the value you set by callerSlots previous getXAttr()
- you constructed callerSlots multi value list with ObjectList.createList()
|
void |
StackFrame.setOperandAttr(Object a)
this replaces all of them - use only if you know
- there will be only one attribute at callerSlots time
- you obtained the value you set by callerSlots previous getXAttr()
- you constructed callerSlots multi value list with ObjectList.createList()
|
abstract void |
DirectCallStackFrame.setReferenceArgument(int idx,
int ref,
Object attr) |
void |
NativeStackFrame.setReferenceArgumentLocal(int idx,
int ref,
Object attr) |
abstract void |
StackFrame.setReferenceArgumentLocal(int idx,
int ref,
Object attr) |
void |
NativeStackFrame.setReturnAttr(Object a) |
void |
MJIEnv.setReturnAttribute(Object attr) |
void |
NativeStackFrame.setReturnValue(Object r) |
static void |
Verify.setShared(Object o,
boolean isShared) |
void |
StackFrame.setSlotAttr(int i,
Object a) |
static void |
Verify.writeObjectToFile(Object object,
String fileName) |
Constructor and Description |
---|
AnnotationInfo.Entry(String key,
Object value) |
Modifier and Type | Class and Description |
---|---|
class |
BreakGenerator
a pseudo CG that is used to break transitions.
|
class |
DoubleChoiceFromList
simple DoubleChoiceGenerator that takes it's values from a single
property "values" (comma or blank separated list)
|
class |
DoubleChoiceFromSet |
class |
DoubleSpec |
class |
DoubleThresholdGenerator
ChoiceGenerator instance that produces a simple 3 value enumeration
|
class |
FloatChoiceFromList |
class |
IntChoiceFromList |
class |
IntChoiceFromSet |
class |
IntIntervalGenerator
Choice Generator that enumerates an interval of int values.
|
class |
InvocationCG
ChoiceGenerator that represents method calls
|
class |
LongChoiceFromList |
class |
NumberChoiceFromList<T extends Number>
common root for list based number choice generators
|
class |
RandomIntIntervalGenerator
a IntChoiceGenerator that randomly chooses a configured number
of values from a specified range
this is usually configured through app properties
<2do> this is too redundant to RandomOrderIntCG - replace
|
class |
RandomOrderIntCG
a generic IntChoiceGenerator randomizer.
|
class |
RandomOrderLongCG |
class |
ThreadChoiceFromSet |
class |
TypedObjectChoice
a choice generator that enumerates the set of all objects of a certain type.
|
Modifier and Type | Method and Description |
---|---|
Object |
ThreadChoiceFromSet.getNextChoiceObject() |
Modifier and Type | Class and Description |
---|---|
class |
AbstractionAdapter
(mostly) pass-through Abstraction
|
class |
AdaptiveSerializer
a CG type adaptive, canonicalizing & filtering serializer that is an
under-approximation mostly aimed at finding data races and deadlocks in programs
with a large number of scheduling points (= thread choices)
This came to bear by accidentally discovering that JPF often seems to finds
concurrency defects by just serializing the thread states, their topmost stack
frames and the objects directly referenced from there.
|
class |
AmmendableFilterConfiguration |
class |
CFSerializer
a FilteringSerializer that performs on-the-fly heap canonicalization to
achieve heap symmetry.
|
class |
DebugCFSerializer
a CFSerializer that stores the serialized program state in a
readable/diffable format.
|
class |
DebugFilteringSerializer
a FilteringSerializer that stores the serialized program state in a
readable/diffable format.
|
class |
DefaultFilterConfiguration |
class |
DynamicAbstractionSerializer
a serializer that uses Abstraction objects stored as field attributes to
obtain the values to hash.
|
class |
DynamicAbstractionSerializer.Attributor |
class |
FieldAmmendmentByName |
class |
FilteringSerializer
serializer that can ignore marked fields and stackframes for state matching
<2do> rework filter policies
|
class |
FramePolicy |
class |
IgnoreConstants
Marks static final field of primitive or known immutable type to be
filtered.
|
class |
Ignored
tag attribute to ignore elements (classes, objects, fields) from
state matching
|
class |
IgnoreReflectiveNames |
class |
IgnoresFromAnnotations |
class |
IgnoreThreadNastiness |
class |
IgnoreUtilSilliness |
class |
IncludesFromAnnotations |
class |
TopFrameSerializer
even more aggressive under-approximation than AdaptiveSerializer.
|
Modifier and Type | Class and Description |
---|---|
class |
File
MJI model class for java.io.File
NOTE - a number of methods are only stubbed out here to make Eclipse compile
JPF code that uses java.io.File (there is no way to tell Eclipse to exclude the
model classes from ths build-path)
|
class |
FileDescriptor
a simple abstraction for a file descriptor, which for us is little more
than just an id for a native data buffer (we don't want to keep the
data itself in the JPF space)
<2do> still needs the standard descriptors
|
class |
FileInputStream
a simple model to read data w/o dragging the file system content into
the JPF memory
|
class |
FileOutputStream |
class |
FilterOutputStream |
class |
InputStream |
class |
InputStreamReader
how hard can it be to transform byte(s) into a char? I hate Unicode
|
class |
OutputStream |
class |
OutputStreamWriter
natively convert char output into byte output
<2do> - this needs to be reworked.
|
class |
PrintStream |
class |
RandomAccessFile
MJI model class for java.io.RandomAccessFile
|
class |
Reader |
class |
Writer |
Modifier and Type | Method and Description |
---|---|
boolean |
File.equals(Object o) |
Modifier and Type | Class and Description |
---|---|
class |
Class<T>
MJI model class for java.lang.Class library abstraction
This is a JPF specific version of a system class because we can't use the real,
platform VM specific version (it's native all over the place, its field
structure isn't documented, most of its methods are private, hence we can't
even instantiate it properly).
|
class |
ClassLoader |
class |
Exception |
class |
Number |
class |
RuntimeException |
class |
StackTraceElement
MJI model class for java.lang.StackTraceElement
|
class |
String
MJI adapter for java.lang.String, based on jdk 1.7.0_07 source.
|
class |
System |
class |
Thread
MJI model class for java.lang.Thread library abstraction
<2do> this should not require the JPF ThreadList to retrieve corresponding ThreadInfos
(the ThreadList might not store terminated threads)
|
class |
Throwable
barebones model class for java.lang.Throwable
the main reason for having one is to defer the stacktrace creation, which
we don't want if all an application does is intercepting a gazillion of
exceptions like NoSuchMethodException
|
Modifier and Type | Method and Description |
---|---|
protected Object |
Object.clone() |
protected Object |
ClassLoader.getClassLoadingLock(String className) |
T[] |
Class.getEnumConstants() |
Object[] |
Class.getSigners() |
Modifier and Type | Method and Description |
---|---|
static void |
System.arraycopy(Object src,
int srcPos,
Object dst,
int dstPos,
int len) |
T |
Class.cast(Object o) |
boolean |
String.equals(Object anObject) |
boolean |
Object.equals(Object o)
default implementation is just an identity check
|
static String |
String.format(Locale l,
String format,
Object... args) |
static String |
String.format(String format,
Object... args) |
static boolean |
Thread.holdsLock(Object obj) |
static int |
System.identityHashCode(Object o) |
boolean |
Class.isInstance(Object o) |
protected void |
ClassLoader.setSigners(Class<?> c,
Object[] signers) |
static String |
String.valueOf(Object x) |
Modifier and Type | Class and Description |
---|---|
class |
Reference<T>
MJI model class for java.lang.ref.Reference library abstraction
we model this so that we can rely on our WeakRefence implementation
|
class |
ReferenceQueue<T>
MJI model class for java.lang.ref.ReferenceQueue library abstraction
|
class |
WeakReference<T>
MJI model class for java.lang.ref.WeakReference library abstraction
|
Modifier and Type | Class and Description |
---|---|
class |
AccessibleObject |
class |
Constructor<T>
(incomplete) support for consructor reflection
pretty stupid - this is almost identical to Method, but we can't derive,
and the delegation happens at the peer level anyways.
|
class |
Field |
class |
InvocationTargetException
not really required to model, but the real thing does some funky
things to override the cause, just making things a bit more complicated
on our VM side (we still init Throwables explicitly from ThreadInfo)
|
class |
Method
minimal Method reflection support.
|
Modifier and Type | Method and Description |
---|---|
Object |
Field.get(Object o) |
Object |
Method.getDefaultValue() |
Object |
Method.invoke(Object object,
Object... args) |
Modifier and Type | Method and Description |
---|---|
boolean |
Method.equals(Object obj) |
boolean |
Field.equals(Object obj) |
boolean |
Constructor.equals(Object obj) |
Object |
Field.get(Object o) |
boolean |
Field.getBoolean(Object o) |
byte |
Field.getByte(Object o) |
char |
Field.getChar(Object o) |
double |
Field.getDouble(Object o) |
float |
Field.getFloat(Object o) |
int |
Field.getInt(Object o) |
long |
Field.getLong(Object o) |
short |
Field.getShort(Object o) |
Object |
Method.invoke(Object object,
Object... args) |
Object |
Method.invoke(Object object,
Object... args) |
T |
Constructor.newInstance(Object... args) |
void |
Field.set(Object o,
Object v) |
void |
Field.setBoolean(Object o,
boolean v) |
void |
Field.setByte(Object o,
byte v) |
void |
Field.setChar(Object o,
char v) |
void |
Field.setDouble(Object o,
double v) |
void |
Field.setFloat(Object o,
float v) |
void |
Field.setInt(Object o,
int val) |
void |
Field.setLong(Object o,
long v) |
void |
Field.setShort(Object o,
short v) |
Modifier and Type | Class and Description |
---|---|
class |
HttpURLConnection |
class |
URLClassLoader |
class |
URLConnection |
class |
URLStreamHandler |
Modifier and Type | Class and Description |
---|---|
class |
AccessController |
class |
MessageDigest
forwarding implementation of MessageDigest.
|
class |
MessageDigestSpi |
class |
SecureClassLoader
This is just a dummy implementation of java.security.SecureClassLoader
|
Modifier and Type | Class and Description |
---|---|
class |
DateFormat |
class |
DecimalFormat
<2do> this class is a Q&D version to get some support for NumberFormats -
something we aren't too interested in yet.
|
class |
Format
(incomplete) model class for java.text.Format
the reason we model this is that we want to cut off all the inner
workings by just delegating to real formatters stored in our
native peer
|
class |
NumberFormat |
class |
SimpleDateFormat
(incomplete) model class for java.text.SimpleDate.
|
Modifier and Type | Method and Description |
---|---|
Object |
Format.parseObject(String source) |
Object |
NumberFormat.parseObject(String source,
ParsePosition pos) |
abstract Object |
Format.parseObject(String source,
ParsePosition pos) |
Modifier and Type | Method and Description |
---|---|
String |
Format.format(Object o) |
abstract StringBuffer |
Format.format(Object o,
StringBuffer sb,
FieldPosition pos) |
StringBuffer |
DecimalFormat.format(Object obj,
StringBuffer toAppendTo,
FieldPosition pos) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractCollection<E> |
class |
AbstractSet<E> |
class |
Dictionary<K,V> |
class |
Hashtable<K,V> |
class |
Properties |
class |
Random |
class |
TimeZone
a concrete TimeZone that forwards to the host VM.
|
class |
TreeSet<E> |
Modifier and Type | Method and Description |
---|---|
Object |
TimeZone.clone() |
Modifier and Type | Class and Description |
---|---|
class |
BrokenBarrierException |
class |
CyclicBarrier
a simplistic CyclicBarrier implementation, required because the real one
relies heavily on Sun infrastructure (including native methods)
|
Modifier and Type | Class and Description |
---|---|
class |
AtomicIntegerArray
model class for AtomicIntegerArray
|
class |
AtomicIntegerFieldUpdater<T>
model class for the AtomicIntegerFieldUpdater
in reality it's an abstract class, but this here is merely a stub anyways
|
class |
AtomicLongArray
model class for AtomicLongArray
|
class |
AtomicLongFieldUpdater<T>
model class for the AtomicLongFieldUpdater
in reality it's an abstract class, but this here is merely a stub anyways
|
class |
AtomicReferenceArray<E>
model class for AtomicReferenceArray
|
class |
AtomicReferenceFieldUpdater<T,V>
model class for the AtomicReferenceFieldUpdater
in reality it's an abstract class, but this here is merely a stub anyways
|
Constructor and Description |
---|
AtomicReferenceArray(E[] array) |
Modifier and Type | Class and Description |
---|---|
class |
FileHandler
simple stub to avoid execptions when using basic logging
|
class |
Handler |
class |
Logger |
class |
StreamHandler |
Modifier and Type | Class and Description |
---|---|
class |
Matcher
model of a regular expression matcher, to save memory and execution time
|
class |
Pattern
simplified model of java.util.refex.Pattern, which otherwise
is very expensive in terms of state memory and execution costs
|
Modifier and Type | Class and Description |
---|---|
static class |
Test.None |
Modifier and Type | Class and Description |
---|---|
class |
AtomicLong
MJI model class for sun.misc.AtomicLong library abstraction
|
class |
Hashing
this is a model class for sun.misc.Hashing, which is a Java 7 class we model
to make JPF compile under Java 6.
|
class |
SharedSecrets
This is a backdoor mechanism in Java 6 to allow (some sort of)
controlled access to internals between packages, using
sun.misc.* interfaces (e.g.
|
class |
Unsafe
Unsafe = unwanted.
|
Modifier and Type | Method and Description |
---|---|
Object |
JavaAWTAccess.get() |
Object |
Unsafe.getObject(Object obj,
int offset)
Deprecated.
|
Object |
Unsafe.getObject(Object obj,
long l) |
Object |
Unsafe.getObjectVolatile(Object obj,
long l) |
Modifier and Type | Method and Description |
---|---|
boolean |
Unsafe.compareAndSwapInt(Object oThis,
long offset,
int expect,
int update) |
boolean |
Unsafe.compareAndSwapLong(Object oThis,
long offset,
long expect,
long update) |
boolean |
Unsafe.compareAndSwapObject(Object oThis,
long offset,
Object expect,
Object update) |
boolean |
Unsafe.getBoolean(Object obj,
int offset)
Deprecated.
|
boolean |
Unsafe.getBoolean(Object obj,
long l) |
boolean |
Unsafe.getBooleanVolatile(Object obj,
long l) |
byte |
Unsafe.getByte(Object obj,
int offset)
Deprecated.
|
byte |
Unsafe.getByte(Object obj,
long l) |
byte |
Unsafe.getByteVolatile(Object obj,
long l) |
char |
Unsafe.getChar(Object obj,
int offset)
Deprecated.
|
char |
Unsafe.getChar(Object obj,
long l) |
char |
Unsafe.getCharVolatile(Object obj,
long l) |
double |
Unsafe.getDouble(Object obj,
int offset)
Deprecated.
|
double |
Unsafe.getDouble(Object obj,
long l) |
double |
Unsafe.getDoubleVolatile(Object obj,
long l) |
float |
Unsafe.getFloat(Object obj,
int offset)
Deprecated.
|
float |
Unsafe.getFloat(Object obj,
long l) |
float |
Unsafe.getFloatVolatile(Object obj,
long l) |
int |
Unsafe.getInt(Object obj,
int offset)
Deprecated.
|
int |
Unsafe.getInt(Object obj,
long l) |
int |
Unsafe.getIntVolatile(Object obj,
long l) |
long |
Unsafe.getLong(Object obj,
int offset)
Deprecated.
|
long |
Unsafe.getLong(Object obj,
long l) |
long |
Unsafe.getLongVolatile(Object obj,
long l) |
Object |
Unsafe.getObject(Object obj,
int offset)
Deprecated.
|
Object |
Unsafe.getObject(Object obj,
long l) |
Object |
Unsafe.getObjectVolatile(Object obj,
long l) |
short |
Unsafe.getShort(Object obj,
int offset)
Deprecated.
|
short |
Unsafe.getShort(Object obj,
long l) |
short |
Unsafe.getShortVolatile(Object obj,
long l) |
void |
JavaAWTAccess.put(Object k,
Object v) |
void |
Unsafe.putBoolean(Object obj,
int offset,
boolean flag)
Deprecated.
|
void |
Unsafe.putBoolean(Object obj,
long l,
boolean flag) |
void |
Unsafe.putBooleanVolatile(Object obj,
long l,
boolean flag) |
void |
Unsafe.putByte(Object obj,
int offset,
byte byte0)
Deprecated.
|
void |
Unsafe.putByte(Object obj,
long l,
byte byte0) |
void |
Unsafe.putByteVolatile(Object obj,
long l,
byte byte0) |
void |
Unsafe.putChar(Object obj,
int offset,
char c)
Deprecated.
|
void |
Unsafe.putChar(Object obj,
long l,
char c) |
void |
Unsafe.putCharVolatile(Object obj,
long l,
char c) |
void |
Unsafe.putDouble(Object obj,
int offset,
double d)
Deprecated.
|
void |
Unsafe.putDouble(Object obj,
long l,
double d) |
void |
Unsafe.putDoubleVolatile(Object obj,
long l,
double d) |
void |
Unsafe.putFloat(Object obj,
int offset,
float f)
Deprecated.
|
void |
Unsafe.putFloat(Object obj,
long l,
float f) |
void |
Unsafe.putFloatVolatile(Object obj,
long l,
float f) |
void |
Unsafe.putInt(Object obj,
int offset,
int i)
Deprecated.
|
void |
Unsafe.putInt(Object obj,
long l,
int i) |
void |
Unsafe.putIntVolatile(Object obj,
long l,
int i) |
void |
Unsafe.putLong(Object obj,
int offset,
long l1)
Deprecated.
|
void |
Unsafe.putLong(Object obj,
long l,
long l1) |
void |
Unsafe.putLongVolatile(Object obj,
long l,
long l1) |
void |
Unsafe.putObject(Object obj,
int offset,
Object obj1)
Deprecated.
|
void |
Unsafe.putObject(Object obj,
long l,
Object obj1) |
void |
Unsafe.putObjectVolatile(Object obj,
long l,
Object obj1) |
void |
Unsafe.putOrderedInt(Object obj,
long l,
int i) |
void |
Unsafe.putOrderedLong(Object obj,
long l,
long l1) |
void |
Unsafe.putOrderedObject(Object obj,
long l,
Object obj1) |
void |
Unsafe.putShort(Object obj,
int offset,
short word0)
Deprecated.
|
void |
Unsafe.putShort(Object obj,
long l,
short word0) |
void |
Unsafe.putShortVolatile(Object obj,
long l,
short word0) |
static int |
Hashing.randomHashSeed(Object o) |
void |
JavaAWTAccess.remove(Object k) |
void |
Unsafe.unpark(Object thread) |
Modifier and Type | Class and Description |
---|---|
class |
ConstantPool
this is a placeholder for a Java 6 class, which we only have here to
support both Java 1.5 and 6 with the same set of env/ classes
see sun.msic.SharedSecrets for details
<2do> THIS IS GOING AWAY AS SOON AS WE OFFICIALLY SWITCH TO JAVA 6
(to be replaced with a native peer for the native methods of the lib class)
|
Modifier and Type | Class and Description |
---|---|
class |
AnnotationType
this is a placeholder for a Java 6 class, which we only have here to
support both Java 1.5 and 6 with the same set of env/ classes
this is Java only, so it's a drag we have to add this, but since it is outside
java.* and doesn't refer to Java 6 stuff outside the sun.misc.SharedSecrets
we bite the bullet and add it (for now)
<2do> THIS IS GOING AWAY AS SOON AS WE OFFICIALLY SWITCH TO JAVA 6
|
Modifier and Type | Method and Description |
---|---|
Map<String,Object> |
AnnotationType.memberDefaults() |