gov.nasa.jpf.listener

Class VarTracker

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.VarTracker

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class VarTracker
extends ListenerAdapter

simple listener tool to find out which variables (locals and fields) are changed how often and from where. This should give a good idea if a state space blows up because of some counter/timer vars, and where to apply the necessary abstractions to close/shrink it

Constructor Summary

Constructors

Constructor and Description
VarTracker(Config config, JPF jpf)

Method Summary

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	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

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, stateBacktracked, stateProcessed, statePurged, stateRestored, 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

VarTracker

public VarTracker(Config config,
                  JPF jpf)

Method Detail

publishPropertyViolation

public void publishPropertyViolation(Publisher publisher)

Specified by:

publishPropertyViolation in interface PublisherExtension

Overrides:

publishPropertyViolation 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

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