gov.nasa.jpf.listener

Class MethodAnalyzer

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.MethodAnalyzer

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

Direct Known Subclasses:

OverlappingMethodAnalyzer

public class MethodAnalyzer
extends ListenerAdapter

analyzes call/execute sequences of methods closely modeled after the DeadlockAnalyzer, i.e. keeps it's own log and doesn't require full instruction trace <2do> this needs to be refactored with DeadlockAnalyzer - the whole trace mgnt (except of the printing) can be made generic

Constructor Summary

Constructors

Constructor and Description
MethodAnalyzer(Config config, JPF jpf)

Method Summary

Modifier and Type	Method and Description
void	instructionExecuted(VM vm, ThreadInfo thread, Instruction nextInsn, Instruction executedInsn) VM has executed the next instruction (can be used to analyze branches, monitor PUTFIELD / GETFIELD and INVOKExx / RETURN instructions)
void	publishPropertyViolation(Publisher publisher)
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	stateRestored(Search search) a previously generated state was restored (can be on a completely different path)
void	stateStored(Search search) somebody stored the state

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, loadClass, methodEntered, methodExited, objectCreated, objectExposed, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectShared, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, publishFinished, publishProbe, publishStart, publishTransition, searchConstraintHit, searchFinished, searchProbed, searchStarted, stateProcessed, statePurged, 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

MethodAnalyzer

public MethodAnalyzer(Config config,
                      JPF jpf)

Method Detail

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

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

stateStored

public void stateStored(Search search)

Description copied from interface: SearchListener

somebody stored the state

Specified by:

stateStored in interface SearchListener

Overrides:

stateStored 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

instructionExecuted

public void instructionExecuted(VM vm,
                                ThreadInfo thread,
                                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

publishPropertyViolation

public void publishPropertyViolation(Publisher publisher)

Specified by:

publishPropertyViolation in interface PublisherExtension

Overrides:

publishPropertyViolation in class ListenerAdapter