gov.nasa.jpf.listener

Class ExceptionInjector

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.ExceptionInjector

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class ExceptionInjector
extends ListenerAdapter

listener to inject exceptions according to user specifications. This tool is meant to be used for exception handler verification, esp. if exceptions thrown by 3rd party code would be hard to produce. Exceptions are specified as a list of xSpec'@'location pairs. ExceptionSpec is specified as a class name, with optional details parameter. If no package is specified, either java.lang or default package are assumed Location can be - class:line - fully qualified method (callee that is supposed to throw, which is NOT executed in this case) - fully qualified method ':' lineOffset for line/offest based locations, either the first or last insn associated with this line (depending on ei.throwFirst=true|false) is not executed but replaced with throwing the exception. Method body line offsets count from the first statement line in the method body Examples: IOException@x.Foobar:42 NullPointerException@x.SomeClass.computeSomething(Ljava/lang/String;I) y.MyException("something went wrong")@x.SomeClass.foo(D):10

Constructor Summary

Constructors

Constructor and Description
ExceptionInjector(Config config, JPF jpf)

Method Summary

Modifier and Type	Method and Description
void	classLoaded(VM vm, ClassInfo loadedClass) get the target insns/methods
void	executeInstruction(VM vm, ThreadInfo ti, Instruction insnToExecute) VM is about to execute the next instruction

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, exceptionBailout, exceptionHandled, exceptionThrown, 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

ExceptionInjector

public ExceptionInjector(Config config,
                         JPF jpf)

Method Detail

classLoaded

public void classLoaded(VM vm,
                        ClassInfo loadedClass)

get the target insns/methods

Specified by:

classLoaded in interface VMListener

Overrides:

classLoaded in class ListenerAdapter

executeInstruction

public void executeInstruction(VM vm,
                               ThreadInfo ti,
                               Instruction insnToExecute)

Description copied from interface: VMListener

VM is about to execute the next instruction

Specified by:

executeInstruction in interface VMListener

Overrides:

executeInstruction in class ListenerAdapter