| 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.
|