gov.nasa.jpf.listener

Class TraceStorer

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.TraceStorer

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class TraceStorer
extends ListenerAdapter

tool to save traces upon various conditions like - property violation - call of a certain method - reaching a certain search depth - creating a certain thread

Constructor Summary

Constructors

Constructor and Description
TraceStorer(Config config, JPF jpf)

Method Summary

Methods

Modifier and Type	Method and Description
void	instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) VM has executed the next instruction (can be used to analyze branches, monitor PUTFIELD / GETFIELD and INVOKExx / RETURN instructions)
void	propertyViolated(Search search) JPF encountered a property violation.
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	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	threadStarted(VM vm, ThreadInfo ti) new Thread entered run() method

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, loadClass, methodEntered, methodExited, objectCreated, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectUnlocked, objectWait, publishConstraintHit, publishFinished, publishPropertyViolation, publishStart, publishTransition, searchFinished, searchStarted, stateBacktracked, stateProcessed, statePurged, stateRestored, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadTerminated, threadWaiting, vmInitialized

Methods inherited from class java.lang.Object

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

Constructor Detail

TraceStorer

public TraceStorer(Config config,
           JPF jpf)

Method Detail

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

Overrides:

propertyViolated 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

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

Overrides:

searchConstraintHit in class ListenerAdapter

instructionExecuted

public void instructionExecuted(VM vm,
                       ThreadInfo ti,
                       Instruction nextInsn,
                       Instruction executedInsn)

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

Overrides:

instructionExecuted in class ListenerAdapter

threadStarted

public void threadStarted(VM vm,
                 ThreadInfo ti)

Description copied from interface: VMListener

new Thread entered run() method

Specified by:

threadStarted in interface VMListener

Overrides:

threadStarted in class ListenerAdapter