gov.nasa.jpf.vm

Class ConstInsnPathTime

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.vm.ConstInsnPathTime

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, TimeModel, VMListener

public class ConstInsnPathTime
extends ListenerAdapter
implements TimeModel

time model that uses instruction count along current path to deduce the execution time. NOTE: the requirement that time has to be strictly increasing along a path means we cannot skip the initialization

Constructor Summary

Constructors

Constructor and Description
ConstInsnPathTime(VM vm, Config conf)

Method Summary

Modifier and Type	Method and Description
void	choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) the next choice was requested from a previously registered ChoiceGenerator NOTE - this notification happens before the KernelState is stored, i.e.
void	choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo ti, Instruction executedInsn) next ChoiceGenerator was registered, which means this is the end of the current transition the reason why we have this in addition to the choiceGeneratorSet is that listeners can reset the registered CG and so force the current transition to continue (although the listener in this case has to make sure the operand stack is in a consistent state for continued execution because there might be a bottom half of an Instruction.execute() missing)
protected long	computeTime()
long	currentTimeMillis()
long	nanoTime()

Methods inherited from class gov.nasa.jpf.ListenerAdapter

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

ConstInsnPathTime

public ConstInsnPathTime(VM vm,
                         Config conf)

Method Detail

computeTime

protected long computeTime()

choiceGeneratorRegistered

public void choiceGeneratorRegistered(VM vm,
                                      ChoiceGenerator<?> nextCG,
                                      ThreadInfo ti,
                                      Instruction executedInsn)

Description copied from interface: VMListener

next ChoiceGenerator was registered, which means this is the end of the current transition the reason why we have this in addition to the choiceGeneratorSet is that listeners can reset the registered CG and so force the current transition to continue (although the listener in this case has to make sure the operand stack is in a consistent state for continued execution because there might be a bottom half of an Instruction.execute() missing)

Specified by:

choiceGeneratorRegistered in interface VMListener

Overrides:

choiceGeneratorRegistered in class ListenerAdapter

choiceGeneratorAdvanced

public void choiceGeneratorAdvanced(VM vm,
                                    ChoiceGenerator<?> currentCG)

Description copied from interface: VMListener

the next choice was requested from a previously registered ChoiceGenerator NOTE - this notification happens before the KernelState is stored, i.e. listeners are NOT allowed to alter the KernelState (e.g. by changing field values or thread states)

Specified by:

choiceGeneratorAdvanced in interface VMListener

Overrides:

choiceGeneratorAdvanced in class ListenerAdapter

currentTimeMillis

public long currentTimeMillis()

Specified by:

currentTimeMillis in interface TimeModel

nanoTime

public long nanoTime()

Specified by:

nanoTime in interface TimeModel