PropertyListenerAdapter

java.lang.Object
- gov.nasa.jpf.GenericProperty
- - gov.nasa.jpf.PropertyListenerAdapter

All Implemented Interfaces:

JPFListener, Property, PublisherExtension, SearchListener, Printable, VMListener, java.lang.Cloneable

Direct Known Subclasses:

AssertionProperty, ErrorTraceGenerator, HeapTracker, IdleFilter, NoStateCycles, NumericValueChecker, PathOutputMonitor, PreciseRaceDetector
```
public abstract class PropertyListenerAdapter
extends GenericProperty
implements SearchListener, VMListener, PublisherExtension
```
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

Constructor Summary

Constructors
Constructor and Description

PropertyListenerAdapter()

Constructors
Constructor and Description
`PropertyListenerAdapter()`

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`boolean`	`check(Search search, VM vm)` return true if property is NOT violated
`void`	`choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG)` the next choice was requested from a previously registered ChoiceGenerator NOTE - this notification happens before the KernelState is stored, i.e.
`void`	`choiceGeneratorProcessed(VM vm, ChoiceGenerator<?> processedCG)` a ChoiceGnerator has returned all his choices NOTE - this notification happens before the KernelState is stored, i.e.
`void`	`choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction)` next ChoiceGenerator was registered, which means this is the end of the current transition the reason why we have this in addition to the choiceGeneratorSet is that listeners can reset the registered CG and so force the current transition to continue (although the listener in this case has to make sure the operand stack is in a consistent state for continued execution because there might be a bottom half of an Instruction.execute() missing)
`void`	`choiceGeneratorSet(VM vm, ChoiceGenerator<?> newCG)` a new ChoiceGenerator was set, which means we are at the beginning of a new transition.
`void`	`classLoaded(VM vm, ClassInfo loadedClass)` new class was loaded.
`Property`	`clone()`
`void`	`exceptionBailout(VM vm, ThreadInfo currentThread)` exception causes top frame to be purged
`void`	`exceptionHandled(VM vm, ThreadInfo currentThread)` exception handled by current top frame
`void`	`exceptionThrown(VM vm, ThreadInfo currentThread, ElementInfo thrownException)` exception was thrown
`void`	`executeInstruction(VM vm, ThreadInfo currentThread, Instruction instructionToExecute)` VM is about to execute the next instruction
`void`	`gcBegin(VM vm)`
`void`	`gcEnd(VM vm)`
`void`	`instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nextInstruction, Instruction executedInstruction)` VM has executed the next instruction (can be used to analyze branches, monitor PUTFIELD / GETFIELD and INVOKExx / RETURN instructions)
`void`	`loadClass(VM vm, ClassFile cf)` a new classfile is about to be parsed.
`void`	`methodEntered(VM vm, ThreadInfo currentThread, MethodInfo enteredMethod)` method body was entered.
`void`	`methodExited(VM vm, ThreadInfo currentThread, MethodInfo exitedMethod)` method body was left.
`void`	`objectCreated(VM vm, ThreadInfo currentThread, ElementInfo newObject)` new object was created
`void`	`objectExposed(VM vm, ThreadInfo currentThread, ElementInfo fieldOwnerObject, ElementInfo exposedObject)` object becomes reachable through a shared reference 'sharedObject' is the (already shared) owner of the field to which the (yet unshared) 'exposedObject' reference got assigned
`void`	`objectLocked(VM vm, ThreadInfo currentThread, ElementInfo lockedObject)` notify if an object lock was taken (this includes automatic surrender during a wait())
`void`	`objectNotify(VM vm, ThreadInfo currentThread, ElementInfo notifyingObject)` notify if an object notifies a single waiter
`void`	`objectNotifyAll(VM vm, ThreadInfo currentThread, ElementInfo notifyingObject)` notify if an object notifies all waiters
`void`	`objectReleased(VM vm, ThreadInfo currentThread, ElementInfo releasedObject)` object was garbage collected (after potential finalization)
`void`	`objectShared(VM vm, ThreadInfo currentThread, ElementInfo sharedObject)` object fields accessed by more than one live thread
`void`	`objectUnlocked(VM vm, ThreadInfo currentThread, ElementInfo unlockedObject)` notify if an object lock was released (this includes automatic reacquisition after a notify())
`void`	`objectWait(VM vm, ThreadInfo currentThread, ElementInfo waitingObject)` notify if a wait() is executed
`void`	`propertyViolated(Search search)` JPF encountered a property violation.
`void`	`publishConstraintHit(Publisher publisher)`
`void`	`publishFinished(Publisher publisher)`
`void`	`publishProbe(Publisher publisher)`
`void`	`publishPropertyViolation(Publisher publisher)`
`void`	`publishStart(Publisher publisher)`
`void`	`publishTransition(Publisher publisher)`
`void`	`reset()`
`void`	`searchConstraintHit(Search search)` there was some contraint hit in the search, we back out could have been turned into a property, but usually is an attribute of the search, not the application
`void`	`searchFinished(Search search)` we're done, either with or without a preceeding error
`void`	`searchProbed(Search search)` there was a probe request, e.g.
`void`	`searchStarted(Search search)` we get this after we enter the search loop, but BEFORE the first forward
`void`	`stateAdvanced(Search search)` got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set
`void`	`stateBacktracked(Search search)` state was backtracked one step
`void`	`stateProcessed(Search search)` state is fully explored
`void`	`statePurged(Search search)` some state is not going to appear in any path anymore
`void`	`stateRestored(Search search)` a previously generated state was restored (can be on a completely different path)
`void`	`stateStored(Search search)` somebody stored the state
`void`	`threadBlocked(VM vm, ThreadInfo blockedThread, ElementInfo lock)` thread waits to acquire a lock // NOTE: vm.getLastThreadInfo() does NOT have to be the running thread, as this // notification can occur as a result of a lock operation in the current thread
`void`	`threadInterrupted(VM vm, ThreadInfo interruptedThread)` thread got interrupted
`void`	`threadNotified(VM vm, ThreadInfo notifiedThread)` thread got notified
`void`	`threadScheduled(VM vm, ThreadInfo scheduledThread)` new thread was scheduled by VM
`void`	`threadStarted(VM vm, ThreadInfo startedThread)` new Thread entered run() method
`void`	`threadTerminated(VM vm, ThreadInfo terminatedThread)` Thread exited run() method
`void`	`threadWaiting(VM vm, ThreadInfo waitingThread)` thread is waiting for signal
`void`	`vmInitialized(VM vm)` VM got initialized (but search is not yet running).

Methods inherited from class gov.nasa.jpf.GenericProperty
getErrorMessage, getExplanation, printOn

Methods inherited from class java.lang.Object
equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Constructor Detail
  - PropertyListenerAdapter
```
public PropertyListenerAdapter()
```
- Method Detail
  - check
```
public boolean check(Search search,
                     VM vm)
```
    Description copied from interface: Property
    
    return true if property is NOT violated
    
    Specified by:
    
    check in interface Property
    
    Specified by:
    
    check in class GenericProperty
  - reset
```
public void reset()
```
    Specified by:
    
    reset in interface Property
    
    Overrides:
    
    reset in class GenericProperty
  - clone
```
public Property clone()
               throws java.lang.CloneNotSupportedException
```
    Specified by:
    
    clone in interface Property
    
    Overrides:
    
    clone in class GenericProperty
    
    Throws:
    
    java.lang.CloneNotSupportedException
  - vmInitialized
```
public void vmInitialized(VM vm)
```
    Description copied from interface: VMListener
    
    VM got initialized (but search is not yet running). This can be used to do type initialization in listeners, since the ClassLoader mechanism is now functional
    
    Specified by:
    
    vmInitialized in interface VMListener
  - instructionExecuted
```
public void instructionExecuted(VM vm,
                                ThreadInfo currentThread,
                                Instruction nextInstruction,
                                Instruction executedInstruction)
```
    Description copied from interface: VMListener
    
    VM has executed the next instruction (can be used to analyze branches, monitor PUTFIELD / GETFIELD and INVOKExx / RETURN instructions)
    
    Specified by:
    
    instructionExecuted in interface VMListener
  - executeInstruction
```
public void executeInstruction(VM vm,
                               ThreadInfo currentThread,
                               Instruction instructionToExecute)
```
    Description copied from interface: VMListener
    
    VM is about to execute the next instruction
    
    Specified by:
    
    executeInstruction in interface VMListener
  - threadStarted
```
public void threadStarted(VM vm,
                          ThreadInfo startedThread)
```
    Description copied from interface: VMListener
    
    new Thread entered run() method
    
    Specified by:
    
    threadStarted in interface VMListener
  - threadWaiting
```
public void threadWaiting(VM vm,
                          ThreadInfo waitingThread)
```
    Description copied from interface: VMListener
    
    thread is waiting for signal
    
    Specified by:
    
    threadWaiting in interface VMListener
  - threadNotified
```
public void threadNotified(VM vm,
                           ThreadInfo notifiedThread)
```
    Description copied from interface: VMListener
    
    thread got notified
    
    Specified by:
    
    threadNotified in interface VMListener
  - threadInterrupted
```
public void threadInterrupted(VM vm,
                              ThreadInfo interruptedThread)
```
    Description copied from interface: VMListener
    
    thread got interrupted
    
    Specified by:
    
    threadInterrupted in interface VMListener
  - threadScheduled
```
public void threadScheduled(VM vm,
                            ThreadInfo scheduledThread)
```
    Description copied from interface: VMListener
    
    new thread was scheduled by VM
    
    Specified by:
    
    threadScheduled in interface VMListener
  - threadBlocked
```
public void threadBlocked(VM vm,
                          ThreadInfo blockedThread,
                          ElementInfo lock)
```
    Description copied from interface: VMListener
    
    thread waits to acquire a lock // NOTE: vm.getLastThreadInfo() does NOT have to be the running thread, as this // notification can occur as a result of a lock operation in the current thread
    
    Specified by:
    
    threadBlocked in interface VMListener
  - threadTerminated
```
public void threadTerminated(VM vm,
                             ThreadInfo terminatedThread)
```
    Description copied from interface: VMListener
    
    Thread exited run() method
    
    Specified by:
    
    threadTerminated in interface VMListener
  - loadClass
```
public void loadClass(VM vm,
                      ClassFile cf)
```
    Description copied from interface: VMListener
    
    a new classfile is about to be parsed. This notification allows replacement of the related classfile data via ClassFile.{get/set}Data() and can be used to do on-the-fly classfile instrumentation with 3rd party libraries
    
    Specified by:
    
    loadClass in interface VMListener
  - classLoaded
```
public void classLoaded(VM vm,
                        ClassInfo loadedClass)
```
    Description copied from interface: VMListener
    
    new class was loaded. This is notified after the ClassInfo has been instantiated, but before the class object is initialized, i.e. clinit is called. The main use for this notification is to identify and store ClassInfos, MethodInfos, FieldInfos or Instructions that are used by listeners etc. in order to enable efficient identify based filters in the performance critical instruction notifications
    
    Specified by:
    
    classLoaded in interface VMListener
  - objectCreated
```
public void objectCreated(VM vm,
                          ThreadInfo currentThread,
                          ElementInfo newObject)
```
    Description copied from interface: VMListener
    
    new object was created
    
    Specified by:
    
    objectCreated in interface VMListener
  - objectReleased
```
public void objectReleased(VM vm,
                           ThreadInfo currentThread,
                           ElementInfo releasedObject)
```
    Description copied from interface: VMListener
    
    object was garbage collected (after potential finalization)
    
    Specified by:
    
    objectReleased in interface VMListener
  - objectLocked
```
public void objectLocked(VM vm,
                         ThreadInfo currentThread,
                         ElementInfo lockedObject)
```
    Description copied from interface: VMListener
    
    notify if an object lock was taken (this includes automatic surrender during a wait())
    
    Specified by:
    
    objectLocked in interface VMListener
  - objectUnlocked
```
public void objectUnlocked(VM vm,
                           ThreadInfo currentThread,
                           ElementInfo unlockedObject)
```
    Description copied from interface: VMListener
    
    notify if an object lock was released (this includes automatic reacquisition after a notify())
    
    Specified by:
    
    objectUnlocked in interface VMListener
  - objectWait
```
public void objectWait(VM vm,
                       ThreadInfo currentThread,
                       ElementInfo waitingObject)
```
    Description copied from interface: VMListener
    
    notify if a wait() is executed
    
    Specified by:
    
    objectWait in interface VMListener
  - objectNotify
```
public void objectNotify(VM vm,
                         ThreadInfo currentThread,
                         ElementInfo notifyingObject)
```
    Description copied from interface: VMListener
    
    notify if an object notifies a single waiter
    
    Specified by:
    
    objectNotify in interface VMListener
  - objectNotifyAll
```
public void objectNotifyAll(VM vm,
                            ThreadInfo currentThread,
                            ElementInfo notifyingObject)
```
    Description copied from interface: VMListener
    
    notify if an object notifies all waiters
    
    Specified by:
    
    objectNotifyAll in interface VMListener
  - objectExposed
```
public void objectExposed(VM vm,
                          ThreadInfo currentThread,
                          ElementInfo fieldOwnerObject,
                          ElementInfo exposedObject)
```
    Description copied from interface: VMListener
    
    object becomes reachable through a shared reference 'sharedObject' is the (already shared) owner of the field to which the (yet unshared) 'exposedObject' reference got assigned
    
    Specified by:
    
    objectExposed in interface VMListener
  - objectShared
```
public void objectShared(VM vm,
                         ThreadInfo currentThread,
                         ElementInfo sharedObject)
```
    Description copied from interface: VMListener
    
    object fields accessed by more than one live thread
    
    Specified by:
    
    objectShared in interface VMListener
  - gcBegin
```
public void gcBegin(VM vm)
```
    Specified by:
    
    gcBegin in interface VMListener
  - gcEnd
```
public void gcEnd(VM vm)
```
    Specified by:
    
    gcEnd in interface VMListener
  - exceptionThrown
```
public void exceptionThrown(VM vm,
                            ThreadInfo currentThread,
                            ElementInfo thrownException)
```
    Description copied from interface: VMListener
    
    exception was thrown
    
    Specified by:
    
    exceptionThrown in interface VMListener
  - exceptionBailout
```
public void exceptionBailout(VM vm,
                             ThreadInfo currentThread)
```
    Description copied from interface: VMListener
    
    exception causes top frame to be purged
    
    Specified by:
    
    exceptionBailout in interface VMListener
  - exceptionHandled
```
public void exceptionHandled(VM vm,
                             ThreadInfo currentThread)
```
    Description copied from interface: VMListener
    
    exception handled by current top frame
    
    Specified by:
    
    exceptionHandled in interface VMListener
  - choiceGeneratorRegistered
```
public void choiceGeneratorRegistered(VM vm,
                                      ChoiceGenerator<?> nextCG,
                                      ThreadInfo currentThread,
                                      Instruction executedInstruction)
```
    Description copied from interface: VMListener
    
    next ChoiceGenerator was registered, which means this is the end of the current transition the reason why we have this in addition to the choiceGeneratorSet is that listeners can reset the registered CG and so force the current transition to continue (although the listener in this case has to make sure the operand stack is in a consistent state for continued execution because there might be a bottom half of an Instruction.execute() missing)
    
    Specified by:
    
    choiceGeneratorRegistered in interface VMListener
  - choiceGeneratorSet
```
public void choiceGeneratorSet(VM vm,
                               ChoiceGenerator<?> newCG)
```
    Description copied from interface: VMListener
    
    a new ChoiceGenerator was set, which means we are at the beginning of a new transition. NOTE - this notification happens before the KernelState is stored, i.e. listeners are NOT allowed to alter the KernelState (e.g. by changing field values or thread states)
    
    Specified by:
    
    choiceGeneratorSet in interface VMListener
  - choiceGeneratorAdvanced
```
public void choiceGeneratorAdvanced(VM vm,
                                    ChoiceGenerator<?> currentCG)
```
    Description copied from interface: VMListener
    
    the next choice was requested from a previously registered ChoiceGenerator NOTE - this notification happens before the KernelState is stored, i.e. listeners are NOT allowed to alter the KernelState (e.g. by changing field values or thread states)
    
    Specified by:
    
    choiceGeneratorAdvanced in interface VMListener
  - choiceGeneratorProcessed
```
public void choiceGeneratorProcessed(VM vm,
                                     ChoiceGenerator<?> processedCG)
```
    Description copied from interface: VMListener
    
    a ChoiceGnerator has returned all his choices NOTE - this notification happens before the KernelState is stored, i.e. listeners are NOT allowed to alter the KernelState (e.g. by changing field values or thread states)
    
    Specified by:
    
    choiceGeneratorProcessed in interface VMListener
  - methodEntered
```
public void methodEntered(VM vm,
                          ThreadInfo currentThread,
                          MethodInfo enteredMethod)
```
    Description copied from interface: VMListener
    
    method body was entered. This is notified before the first instruction is executed
    
    Specified by:
    
    methodEntered in interface VMListener
  - methodExited
```
public void methodExited(VM vm,
                         ThreadInfo currentThread,
                         MethodInfo exitedMethod)
```
    Description copied from interface: VMListener
    
    method body was left. This is notified after the last instruction had been executed NOTE - this is also notified when a StackFrame is dropped due to unhandled exceptions
    
    Specified by:
    
    methodExited in interface VMListener
  - stateAdvanced
```
public void stateAdvanced(Search search)
```
    Description copied from interface: SearchListener
    
    got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set
    
    Specified by:
    
    stateAdvanced in interface SearchListener
  - stateProcessed
```
public void stateProcessed(Search search)
```
    Description copied from interface: SearchListener
    
    state is fully explored
    
    Specified by:
    
    stateProcessed in interface SearchListener
  - stateBacktracked
```
public void stateBacktracked(Search search)
```
    Description copied from interface: SearchListener
    
    state was backtracked one step
    
    Specified by:
    
    stateBacktracked in interface SearchListener
  - statePurged
```
public void statePurged(Search search)
```
    Description copied from interface: SearchListener
    
    some state is not going to appear in any path anymore
    
    Specified by:
    
    statePurged in interface SearchListener
  - stateStored
```
public void stateStored(Search search)
```
    Description copied from interface: SearchListener
    
    somebody stored the state
    
    Specified by:
    
    stateStored in interface SearchListener
  - stateRestored
```
public void stateRestored(Search search)
```
    Description copied from interface: SearchListener
    
    a previously generated state was restored (can be on a completely different path)
    
    Specified by:
    
    stateRestored in interface SearchListener
  - searchProbed
```
public void searchProbed(Search search)
```
    Description copied from interface: SearchListener
    
    there was a probe request, e.g. from a periodical timer note this is called synchronously from within the JPF execution loop (after instruction execution)
    
    Specified by:
    
    searchProbed in interface SearchListener
  - propertyViolated
```
public void propertyViolated(Search search)
```
    Description copied from interface: SearchListener
    
    JPF encountered a property violation. Note - this is always preceeded by a stateAdvanced
    
    Specified by:
    
    propertyViolated in interface SearchListener
  - searchStarted
```
public void searchStarted(Search search)
```
    Description copied from interface: SearchListener
    
    we get this after we enter the search loop, but BEFORE the first forward
    
    Specified by:
    
    searchStarted in interface SearchListener
  - searchConstraintHit
```
public void searchConstraintHit(Search search)
```
    Description copied from interface: SearchListener
    
    there was some contraint hit in the search, we back out could have been turned into a property, but usually is an attribute of the search, not the application
    
    Specified by:
    
    searchConstraintHit in interface SearchListener
  - searchFinished
```
public void searchFinished(Search search)
```
    Description copied from interface: SearchListener
    
    we're done, either with or without a preceeding error
    
    Specified by:
    
    searchFinished in interface SearchListener
  - publishStart
```
public void publishStart(Publisher publisher)
```
    Specified by:
    
    publishStart in interface PublisherExtension
  - publishTransition
```
public void publishTransition(Publisher publisher)
```
    Specified by:
    
    publishTransition in interface PublisherExtension
  - publishPropertyViolation
```
public void publishPropertyViolation(Publisher publisher)
```
    Specified by:
    
    publishPropertyViolation in interface PublisherExtension
  - publishConstraintHit
```
public void publishConstraintHit(Publisher publisher)
```
    Specified by:
    
    publishConstraintHit in interface PublisherExtension
  - publishFinished
```
public void publishFinished(Publisher publisher)
```
    Specified by:
    
    publishFinished in interface PublisherExtension
  - publishProbe
```
public void publishProbe(Publisher publisher)
```
    Specified by:
    
    publishProbe in interface PublisherExtension

Class PropertyListenerAdapter

Constructor Summary

Method Summary

Methods inherited from class gov.nasa.jpf.GenericProperty

Methods inherited from class java.lang.Object

Constructor Detail

PropertyListenerAdapter

Method Detail

check

reset

clone

vmInitialized

instructionExecuted

executeInstruction

threadStarted

threadWaiting

threadNotified

threadInterrupted

threadScheduled

threadBlocked

threadTerminated

loadClass

classLoaded

objectCreated

objectReleased

objectLocked

objectUnlocked

objectWait

objectNotify

objectNotifyAll

objectExposed

objectShared

gcBegin

gcEnd

exceptionThrown

exceptionBailout

exceptionHandled

choiceGeneratorRegistered

choiceGeneratorSet

choiceGeneratorAdvanced

choiceGeneratorProcessed

methodEntered

methodExited

stateAdvanced

stateProcessed

stateBacktracked

statePurged

stateStored

stateRestored

searchProbed

propertyViolated

searchStarted

searchConstraintHit

searchFinished

publishStart

publishTransition

publishPropertyViolation

publishConstraintHit

publishFinished

publishProbe