gov.nasa.jpf.listener

Class CoverageAnalyzer

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.listener.CoverageAnalyzer

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener

public class CoverageAnalyzer
extends ListenerAdapter
implements PublisherExtension

a listener to report coverage statistics The idea is to collect per-class/-method/-thread information about executed instructions, and then analyze this deeper when it comes to report time (e.g. branch coverage, basic blocks, ..) Keep in mind that this is potentially a concurrent, model checked program, i.e. there is more to coverage than what hits the eye of a static analyzer (exceptions, data and thread CGs)

Constructor Summary

Constructors

Constructor and Description
CoverageAnalyzer(Config conf, JPF jpf)

Method Summary

Modifier and Type	Method and Description
void	choiceGeneratorSet(VM vm, ChoiceGenerator<?> newCG) a new ChoiceGenerator was set, which means we are at the beginning of a new transition.
void	classLoaded(VM vm, ClassInfo ci) print uncovered source ranges
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	publishFinished(Publisher publisher)

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, loadClass, methodEntered, methodExited, objectCreated, objectExposed, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectShared, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, 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

Methods inherited from interface gov.nasa.jpf.report.PublisherExtension

publishConstraintHit, publishProbe, publishPropertyViolation, publishStart, publishTransition

Constructor Detail

CoverageAnalyzer

public CoverageAnalyzer(Config conf,
                        JPF jpf)

Method Detail

classLoaded

public void classLoaded(VM vm,
                        ClassInfo ci)

print uncovered source ranges

Specified by:

classLoaded in interface VMListener

Overrides:

classLoaded 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

choiceGeneratorSet

public void choiceGeneratorSet(VM vm,
                               ChoiceGenerator<?> newCG)

Description copied from interface: VMListener

a new ChoiceGenerator was set, which means we are at the beginning of a new transition. 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:

choiceGeneratorSet in interface VMListener

Overrides:

choiceGeneratorSet in class ListenerAdapter

publishFinished

public void publishFinished(Publisher publisher)

Specified by:

publishFinished in interface PublisherExtension

Overrides:

publishFinished in class ListenerAdapter