Package | Description |
---|---|
gov.nasa.jpf.vm | |
gov.nasa.jpf.vm.serialize |
Modifier and Type | Interface and Description |
---|---|
interface |
IncrementalChangeTracker
This should be implemented by classes that read & reset "hasChanged"-type
information in the KernelState.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractRestorer<Saved> |
class |
AbstractSerializer |
class |
DefaultMementoRestorer
a MementoRestorer that uses the default mementos
|
class |
MementoRestorer
state storer/restorer that works solely on a snapshot basis
|
Modifier and Type | Method and Description |
---|---|
void |
KernelState.pushChangeListener(KernelState.ChangeListener cl)
push a listener for notification of the next change.
|
Modifier and Type | Class and Description |
---|---|
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 |
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 |
DynamicAbstractionSerializer
a serializer that uses Abstraction objects stored as field attributes to
obtain the values to hash.
|
class |
FilteringSerializer
serializer that can ignore marked fields and stackframes for state matching
<2do> rework filter policies
|
class |
TopFrameSerializer
even more aggressive under-approximation than AdaptiveSerializer.
|