gov.nasa.jpf.listener

Class EndlessLoopDetector

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.listener.IdleFilter

gov.nasa.jpf.listener.EndlessLoopDetector

All Implemented Interfaces:

JPFListener, Property, PublisherExtension, SearchListener, Printable, VMListener, java.lang.Cloneable

public class EndlessLoopDetector
extends IdleFilter

little listener that tries to detect endless while() loops by counting backjumps, breaking transitions if the count exceeds a threshold, and then checking if program states match. If they do, there would be no progress in this thread.

Constructor Summary

Constructors

Constructor and Description
EndlessLoopDetector(Config config)

Method Summary

Modifier and Type	Method and Description
boolean	check(Search search, VM vm) return true if property is NOT violated
void	reset()
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.listener.IdleFilter

instructionExecuted, stateBacktracked, threadTerminated

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, clone, 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, stateProcessed, statePurged, stateRestored, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadWaiting, vmInitialized

Methods inherited from class gov.nasa.jpf.GenericProperty

getErrorMessage, getExplanation, printOn

Methods inherited from class java.lang.Object

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

Constructor Detail

EndlessLoopDetector

public EndlessLoopDetector(Config config)

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 IdleFilter

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