gov.nasa.jpf.listener

Class BudgetChecker

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.BudgetChecker

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class BudgetChecker
extends ListenerAdapter

Listener that implements various budget constraints

Constructor Summary

Constructors

Constructor and Description
BudgetChecker(Config conf, JPF jpf)

Method Summary

Modifier and Type	Method and Description
boolean	depthExceeded()
boolean	heapExceeded()
boolean	insnExceeded()
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)
boolean	newStatesExceeded()
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
boolean	statesExceeded()
boolean	timeExceeded()

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

BudgetChecker

public BudgetChecker(Config conf,
                     JPF jpf)

Method Detail

timeExceeded

public boolean timeExceeded()

heapExceeded

public boolean heapExceeded()

depthExceeded

public boolean depthExceeded()

statesExceeded

public boolean statesExceeded()

insnExceeded

public boolean insnExceeded()

newStatesExceeded

public boolean newStatesExceeded()

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