gov.nasa.jpf.listener

Class ObjectTracker

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.listener.ObjectTracker

All Implemented Interfaces:

JPFListener, Property, PublisherExtension, SearchListener, Printable, VMListener

public class ObjectTracker
extends PropertyListenerAdapter

listener that keeps track of all allocations, method calls, field updates and deallocations of instances of a set of types we don't need a StateExtensionClient/Listener here because we only keep live, typed object data. If we ever backtrack to a point where a registered object didn't exist yet, this id can't be used again (for a relevant object) w/o previous registration. Note this might cause some discarded objects to stay around, but requires probably less memory than storing a collection for every state id.

Constructor Summary

Constructors

Constructor and Description
ObjectTracker(Config conf, JPF jpf)

Method Summary

Methods

Modifier and Type	Method and Description
boolean	check(Search search, VM vm) return true if property is NOT violated
String	getErrorMessage()
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	objectCreated(VM vm, ThreadInfo ti, ElementInfo ei) new object was created
void	objectReleased(VM vm, ThreadInfo ti, ElementInfo ei) object was garbage collected (after potential finalization)
void	reset()

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

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

Methods inherited from class gov.nasa.jpf.GenericProperty

getExplanation, printOn

Methods inherited from class java.lang.Object

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

Constructor Detail

ObjectTracker

public ObjectTracker(Config conf,
             JPF jpf)

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

Overrides:

check in class PropertyListenerAdapter

reset

public void reset()

Specified by:

reset in interface Property

Overrides:

reset in class PropertyListenerAdapter

getErrorMessage

public String getErrorMessage()

Specified by:

getErrorMessage in interface Property

Overrides:

getErrorMessage in class GenericProperty

objectCreated

public void objectCreated(VM vm,
                 ThreadInfo ti,
                 ElementInfo ei)

Description copied from interface: VMListener

new object was created

Specified by:

objectCreated in interface VMListener

Overrides:

objectCreated in class PropertyListenerAdapter

objectReleased

public void objectReleased(VM vm,
                  ThreadInfo ti,
                  ElementInfo ei)

Description copied from interface: VMListener

object was garbage collected (after potential finalization)

Specified by:

objectReleased in interface VMListener

Overrides:

objectReleased in class PropertyListenerAdapter

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 PropertyListenerAdapter