Package | Description |
---|---|
gov.nasa.jpf | |
gov.nasa.jpf.listener | |
gov.nasa.jpf.util | |
gov.nasa.jpf.vm |
Modifier and Type | Interface and Description |
---|---|
interface |
Property
abstraction that is used by Search objects to determine if program
properties have been violated (e.g.
|
Modifier and Type | Class and Description |
---|---|
class |
GenericProperty
generic abstract base class implementing program properties.
|
class |
PropertyListenerAdapter
abstract base class that dummy implements Property, Search- and VMListener methods
convenient for creating listeners that act as properties, just having to override
the methods they need
the only local functionality is that instances register themselves automatically
as property when the search is started
<2do> rewrite once GenericProperty is an interface
|
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.
|
Modifier and Type | Method and Description |
---|---|
static void |
Debug.print(int l,
int k,
Printable p) |
static void |
Debug.print(int l,
Printable p) |
static void |
Debug.println(int l,
int k,
Printable p) |
static void |
Debug.println(int l,
Printable p) |
Modifier and Type | Class and Description |
---|---|
class |
NoOutOfMemoryErrorProperty
A property class so that gov.nasa.jpf.JPF can add an error to the
gov.nasa.jpf.search.Search object when JPF catches an OutOfMemoryError.
|
class |
NotDeadlockedProperty
property class to check for no-runnable-threads conditions
|
class |
NoUncaughtExceptionsProperty
property class to check for uncaught exceptions
|
class |
Path
Path represents the data structure in which a execution trace is recorded.
|
class |
UncaughtException
represents the case of an unhandled exception detected by JPF
This is a "controlflow exception", but I finally made my peace with it since
UncaughtExceptions can be thrown from various places, including the VM (
|