gov.nasa.jpf.listener

Class LockedStackDepth

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.LockedStackDepth

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class LockedStackDepth
extends ListenerAdapter

A listener that tracks information about the stack depth of when a lock is first acquired. If Writing a test for this class is very difficult. Hence, a lot of asserts are added.

Constructor Summary

Constructors

Constructor and Description
LockedStackDepth()

Method Summary

Methods

Modifier and Type	Method and Description
List<ElementInfo>	getLockedInTopFrame(ThreadInfo thread)
int	getLockedStackDepth(ElementInfo lock)
void	objectLocked(VM vm, ThreadInfo thread, ElementInfo ei) notify if an object lock was taken (this includes automatic surrender during a wait())
void	objectUnlocked(VM vm, ThreadInfo thread, ElementInfo ei) notify if an object lock was released (this includes automatic reacquisition after a notify())
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	stateRestored(Search search) a previously generated state was restored (can be on a completely different path)

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, instructionExecuted, loadClass, methodEntered, methodExited, objectCreated, objectNotify, objectNotifyAll, objectReleased, objectWait, propertyViolated, publishConstraintHit, publishFinished, publishPropertyViolation, publishStart, publishTransition, searchConstraintHit, searchFinished, statePurged, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadTerminated, threadWaiting, vmInitialized

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

LockedStackDepth

public LockedStackDepth()

Method Detail

getLockedStackDepth

public int getLockedStackDepth(ElementInfo lock)

getLockedInTopFrame

public List<ElementInfo> getLockedInTopFrame(ThreadInfo thread)

objectLocked

public void objectLocked(VM vm,
                ThreadInfo thread,
                ElementInfo ei)

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

Overrides:

objectLocked in class ListenerAdapter

objectUnlocked

public void objectUnlocked(VM vm,
                  ThreadInfo thread,
                  ElementInfo ei)

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

Overrides:

objectUnlocked in class ListenerAdapter

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

Overrides:

searchStarted in class ListenerAdapter

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

Overrides:

stateAdvanced in class ListenerAdapter

stateProcessed

public void stateProcessed(Search search)

Description copied from interface: SearchListener

state is fully explored

Specified by:

stateProcessed in interface SearchListener

Overrides:

stateProcessed in class ListenerAdapter

stateBacktracked

public void stateBacktracked(Search search)

Description copied from interface: SearchListener

state was backtracked one step

Specified by:

stateBacktracked in interface SearchListener

Overrides:

stateBacktracked in class ListenerAdapter

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

Overrides:

stateRestored in class ListenerAdapter