listener for gov.nasa.jpf.Config changes.
this is just a common root type for VMListeners and SearchListeners.
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
abstraction that is used by Search objects to determine if program properties have been violated (e.g.
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(..)
if this class can be loaded, the JPF core is in the CLASSPATH.
common stuff used by all Annotation Proxies
this is just a very rough abstraction at this point, which only supports reading static URL contents.
class that encapsulates property-based JPF configuration.
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.
class used to store property violations (property and path)
generic abstract base class implementing program properties.
main class of the JPF verification framework.
classloader that is used by Config to instantiate from JPF configured paths.
Adapter class that dummy implements both VMListener and SearchListener interfaces Used to ease implementation of listeners that only process a few notifications
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
abstraction of JPF execution state that can be queried and stored by listeners
private helper class for local termination of JPF (without killing the whole Java process via System.exit).
this class wraps the various exceptions we might encounter during initialization and use of Config
internal JPF error
common root for all exceptions thrown by JPF
JPFException that wraps whatever can go wrong in a listener during notification
JPFException that wraps whatever can go wrong in a native method