Package gov.nasa.jpf

Interface Summary

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 (Config) ctor so that they don't need to obtain a new Config object.
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 Summary

Class	Description
$coreTag	if this class can be loaded, the JPF core is in the CLASSPATH.
AnnotationProxyBase	common stuff used by all Annotation Proxies
BoxObjectCaches
CachedROHttpConnection	this is just a very rough abstraction at this point, which only supports reading static URL contents.
Config	class that encapsulates property-based JPF configuration.
ConsoleOutputStream	this is what we use for System.out and System.err, hence we go native as quickly as possible, hence we don't need an underlying stream.
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
SerializationConstructor<T>
State	abstraction of JPF execution state that can be queried and stored by listeners

Enum Summary

Enum	Description
JPF.Status

Exception Summary

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