Class and Description |
---|
JPFLogger
this is a decorator for java.util.logging.JPFLogger
We use this to avoid explicit Logger.isLoggable() checks in the code.
|
Printable
Printable is mainly used to avoid having to create potentially huge
String(via StringBuilders or Writers) which are just used to be
written to std streams
|
Class and Description |
---|
Invocation
a record that includes all information to perform a call
|
Class and Description |
---|
Invocation
a record that includes all information to perform a call
|
Class and Description |
---|
LocationSpec
support for specification of source locations
This maps sourcefile:line1-range strings into instructions that can be efficiently
checked for by listeners.
|
MethodSpec
utility class that can match methods/args against specs.
|
Printable
Printable is mainly used to avoid having to create potentially huge
String(via StringBuilders or Writers) which are just used to be
written to std streams
|
Class and Description |
---|
IntVector
(more efficient?) alternative to Vector
|
JPFLogger
this is a decorator for java.util.logging.JPFLogger
We use this to avoid explicit Logger.isLoggable() checks in the code.
|
Class and Description |
---|
ArrayIntSet
common base for array based IntSet implementations
|
BitArray
Faster version of BitSet for fixed size.
|
BitSet1024
a fixed size BitSet with 1024 bits.
|
BitSet256
a fixed size BitSet with 256 bits.
|
BitSet64 |
Cloner
this is a helper to enable deep copy of generic containers, where the
element types are generic type parameters and therefore can't be
created via ctor or clone.
|
ElementCreator
create an instance of type E out of a T instance
|
FeatureSpec
common base class for MethodSpec and FieldSpec
|
FieldSpec
utility class that can match FieldInfos against specs.
|
FinalBitSet
Faster version of BitSet for those that never change.
|
FixedBitSet
BitSet like interface for fixed size bit sets
|
Growth |
HashData
object to compute complex hash values that can be accumulated and
delegated (to aggregates etc.)
used to obtain hashcodes for states
|
HashPool
data structure used to do hash collapsing.
|
IdentityObjectSet
an ObjectSet that uses reference comparison (identity) for inclusion checks
|
ImmutableList
utility class for JPF internal linked lists that are tail-immutable
|
IndexIterator
specialized iterator class for index values [0..N]
|
IntIterator
just a little helper to iterate over collections of ints without doing
a lot of boxing/unboxing
|
IntSet |
IntTable
A hash map that holds int values associated with generic key objects.
|
IntTable.Entry
encapsulates an Entry in the table.
|
IntTable.Snapshot
helper class to store a compact, invariant representation of this table
|
IntVector
(more efficient?) alternative to Vector
|
JPFLogger
this is a decorator for java.util.logging.JPFLogger
We use this to avoid explicit Logger.isLoggable() checks in the code.
|
LocationSpec
support for specification of source locations
This maps sourcefile:line1-range strings into instructions that can be efficiently
checked for by listeners.
|
LogHandler
log handler class that deals with output selection and formatting.
|
LongVector
(more efficient?) alternative to Vector
|
MethodSpec
utility class that can match methods/args against specs.
|
MutableInteger
an object that holds a mutable int.
|
ObjArray
Wrapper for arrays of objects which provides proper equals() and hashCode()
methods, and behaves nicely with Java 1.5 generics.
|
ObjectList.Iterator |
ObjectList.TypedIterator |
ObjectQueue
generic interface for object queues
|
ObjectSet
generic interface for object sets
this one makes no guarantees about identity or value comparison
|
ObjVector
more customizable alternative to java.util.Vector.
|
ObjVector.MutatingSnapshot
snapshot that can mutate element values, but therefore can't use block operations.
|
ObjVector.Snapshot
this is a block operation snapshot that stores chunks of original data with
not more than DEFAULT_MAX_GAP consecutive null elements.
|
Pair
simple const wrapper utility class for 2-tuple
|
Predicate |
Printable
Printable is mainly used to avoid having to create potentially huge
String(via StringBuilders or Writers) which are just used to be
written to std streams
|
Processor |
PSIntMap
Persistent (immutable) associative array that maps integer keys to generic reference values.
|
PSIntMap.Node
Abstract root class for all node types.
|
ReadOnlyObjList |
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.
|
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
|
RunListener
little helper interface to facilitate resetting classes and objects
between JPF runs, mostly to avoid memory leaks
|
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.
|
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
|
SourceRef
a source reference abstraction wrapping file and line information
|
SparseClusterArray
A generic sparse reference array that assumes clusters, and more
frequent intra-cluster access.
|
SparseClusterArray.Chunk |
SparseClusterArray.ChunkNode |
SparseClusterArray.Entry |
SparseClusterArray.Node
this corresponds to a toplevel cluster (e.g.
|
SparseClusterArray.Root |
SparseClusterArray.Snapshot |
SparseIntVector
This has approximately the interface of IntVector but uses a hash table
instead of an array.
|
SparseIntVector.Snapshot
a simplistic snapshot implementation that stores set indices/values in order to save space
|
StateExtensionClient
generic interface for state extensions that have to be backtracked/restored
|
StringMatcher
simple wrapper around Patter/Matcher pairs, with patterns using '*' wildcards
same as StringSetMatcher but for single patterns
|
StringSetMatcher
simple utility that can be used to check for string matches in
sets with '*' wildcards, e.g.
|
Trace
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
|
TraceElement
encapsulates a listener-managed trace operation
|
Transformer
transforms between two types
a utility interface that esp.
|
TwoTypeComparator
like a normal comparator, but comparing heterogenous objects
|
TypeSpec
wildcard supporting type specification to be used for JPF configuration.
|
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 and Description |
---|
StateExtensionClient
generic interface for state extensions that have to be backtracked/restored
|
Class and Description |
---|
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 and Description |
---|
ArrayIntSet
common base for array based IntSet implementations
|
FinalBitSet
Faster version of BitSet for those that never change.
|
FixedBitSet
BitSet like interface for fixed size bit sets
|
HashData
object to compute complex hash values that can be accumulated and
delegated (to aggregates etc.)
used to obtain hashcodes for states
|
ImmutableList
utility class for JPF internal linked lists that are tail-immutable
|
IntSet |
IntTable
A hash map that holds int values associated with generic key objects.
|
IntVector
(more efficient?) alternative to Vector
|
JPFLogger
this is a decorator for java.util.logging.JPFLogger
We use this to avoid explicit Logger.isLoggable() checks in the code.
|
LocationSpec
support for specification of source locations
This maps sourcefile:line1-range strings into instructions that can be efficiently
checked for by listeners.
|
MethodSpec
utility class that can match methods/args against specs.
|
ObjectList.Iterator |
ObjectList.TypedIterator |
ObjectQueue
generic interface for object queues
|
ObjVector
more customizable alternative to java.util.Vector.
|
Predicate |
Printable
Printable is mainly used to avoid having to create potentially huge
String(via StringBuilders or Writers) which are just used to be
written to std streams
|
Processor |
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
|
SparseObjVector
This has approximately the interface of ObjVector but uses a hash table
instead of an array.
|
UnsortedArrayIntSet
a simplistic IntSet implementation that uses an unsorted array to keep elements.
|
Class and Description |
---|
Invocation
a record that includes all information to perform a call
|
Class and Description |
---|
FinalBitSet
Faster version of BitSet for those that never change.
|
IntVector
(more efficient?) alternative to Vector
|
ObjectQueue
generic interface for object queues
|
ObjVector
more customizable alternative to java.util.Vector.
|
Processor |
StringSetMatcher
simple utility that can be used to check for string matches in
sets with '*' wildcards, e.g.
|