Interface | Description |
---|---|
ConfigChangeListener |
listener for gov.nasa.jpf.Config changes.
|
JPFListener |
this is just a common root type for VMListeners and SearchListeners.
|
JPFShell |
type that can be used to instantiate and run a JPF object
Shell objects can be configured via the JPF 'shell' property, and are
typically JPF user interface implementations
Instantiation and start() call are done from the JPF.main() method
Usually, JPFShell implementors have a
|
Property |
abstraction that is used by Search objects to determine if program
properties have been violated (e.g.
|
StateExtension | |
SystemAttribute |
a type tag for attributes used by JPF
SystemAttributes are protected by the .util.ObjectList API against accidental
set(..) overwrite, they have to be removed by forceSet(..)
|
Class | Description |
---|---|
$coreTag |
if this class can be loaded, the JPF core is in the CLASSPATH.
|
Config |
class that encapsulates property-based JPF configuration.
|
Error |
class used to store property violations (property and path)
|
GenericProperty |
generic abstract base class implementing program properties.
|
JPF |
main class of the JPF verification framework.
|
JPFClassLoader |
classloader that is used by Config to instantiate from JPF configured
paths.
|
ListenerAdapter |
Adapter class that dummy implements both VMListener and SearchListener interfaces
Used to ease implementation of listeners that only process a few notifications
|
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
|
State |
abstraction of JPF execution state that can be queried and stored by
listeners
|
Enum | Description |
---|---|
JPF.Status |
Exception | Description |
---|---|
JPF.ExitException |
private helper class for local termination of JPF (without killing the
whole Java process via System.exit).
|
JPFConfigException |
this class wraps the various exceptions we might encounter during
initialization and use of Config
|
JPFErrorException |
internal JPF error
|
JPFException |
common root for all exceptions thrown by JPF
|
JPFListenerException |
JPFException that wraps whatever can go wrong in a listener during notification
|
JPFNativePeerException |
JPFException that wraps whatever can go wrong in a native method
|