| Interface | Description |
|---|---|
| Abstraction |
interface to abstract concrete primitive values for the sake of state matching
|
| AmmendableFilterConfiguration.Ammendment | |
| AmmendableFilterConfiguration.FieldAmmendment | |
| AmmendableFilterConfiguration.FrameAmmendment | |
| AmmendableFilterConfiguration.InstanceAmmendment | |
| AmmendableFilterConfiguration.InstanceOverride | |
| AmmendableFilterConfiguration.StaticAmmendment | |
| FilterConfiguration |
| Class | Description |
|---|---|
| AbstractionAdapter |
(mostly) pass-through Abstraction
|
| 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.
|
| AmmendableFilterConfiguration | |
| CFSerializer |
a FilteringSerializer that performs on-the-fly heap canonicalization to
achieve heap symmetry.
|
| DebugCFSerializer |
a CFSerializer that stores the serialized program state in a
readable/diffable format.
|
| DebugFilteringSerializer |
a FilteringSerializer that stores the serialized program state in a
readable/diffable format.
|
| DefaultFilterConfiguration | |
| DynamicAbstractionSerializer |
a serializer that uses Abstraction objects stored as field attributes to
obtain the values to hash.
|
| FieldAmmendmentByName | |
| FilteringSerializer |
serializer that can ignore marked fields and stackframes for state matching
<2do> rework filter policies
|
| FramePolicy | |
| IgnoreConstants |
Marks static final field of primitive or known immutable type to be
filtered.
|
| Ignored |
tag attribute to ignore elements (classes, objects, fields) from
state matching
|
| IgnoreReflectiveNames | |
| IgnoresFromAnnotations | |
| IgnoreThreadNastiness | |
| IgnoreUtilSilliness | |
| IncludesFromAnnotations | |
| TopFrameSerializer |
even more aggressive under-approximation than AdaptiveSerializer.
|
| Exception | Description |
|---|---|
| UnknownJPFClass |
exception to indicate that JPF can't find a (model) class of a given name
For native clients directly or indirectly cause class resolution
<2do> we might turn this into an handled exception at some point
|
| Annotation Type | Description |
|---|---|
| FilterFrame |
USE CAREFULLY - Indicates that the stack frame of a method should not,
in specified ways, be considered during state matching.
|
| UnfilterField |
Indicates that a field in the model SHOULD BE considered during
state matching, even if other (prior) configuration would filter it.
|