gov.nasa.jpf.listener

Class NumericValueChecker

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.listener.NumericValueChecker

All Implemented Interfaces:

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

public class NumericValueChecker
extends PropertyListenerAdapter

little listener that checks value ranges of specified numeric fields and local vars configuration examples: range.fields=speed,.. range.speed.field=x.y.SomeClass.velocity range.speed.min=300 range.speed.max=500 range.vars=altitude,.. range.altitude.var=x.y.SomeClass.computeTrajectory(int):a range.altitude.min=125000

Constructor Summary

Constructors

Constructor and Description
NumericValueChecker(Config conf)

Method Summary

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

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

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

Constructor Detail

NumericValueChecker

public NumericValueChecker(Config conf)

Method Detail

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

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 java.lang.String getErrorMessage()

Specified by:

getErrorMessage in interface Property

Overrides:

getErrorMessage in class GenericProperty