Package | Description |
---|---|
gov.nasa.jpf | |
gov.nasa.jpf.listener |
Modifier and Type | Method and Description |
---|---|
void |
JPF.addPropertyListener(PropertyListenerAdapter pl) |
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 |
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 |
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 |
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 |
PathOutputMonitor
listener that monitors path output, matching it against specifications
supplied as text files.
|
class |
PreciseRaceDetector
This is a Race Detection Algorithm that is precise in its calculation of races, i.e.
|