gov.nasa.jpf.listener

Class ErrorTraceGenerator

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.listener.ErrorTraceGenerator

All Implemented Interfaces:

JPFListener, Property, PublisherExtension, SearchListener, Printable, VMListener

public class ErrorTraceGenerator
extends PropertyListenerAdapter
implements PublisherExtension

A lightweight listener to generate the error trace by printing the program instructions at transition boundaries. The idea is to have a shorter trace output that only shows the choices

Field Summary

Fields

Modifier and Type	Field and Description
protected boolean	showInsn
protected boolean	showLoc
protected boolean	showSrc
protected ChoiceGenerator<?>[]	trace

Constructor Summary

Constructors

Constructor and Description
ErrorTraceGenerator(Config conf, JPF jpf)

Method Summary

Methods

Modifier and Type	Method and Description
void	propertyViolated(Search search) JPF encountered a property violation.
void	publishPropertyViolation(Publisher p)

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

check, choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, instructionExecuted, loadClass, methodEntered, methodExited, objectCreated, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectUnlocked, objectWait, publishConstraintHit, publishFinished, publishStart, publishTransition, reset, searchConstraintHit, searchFinished, searchStarted, stateAdvanced, stateBacktracked, stateProcessed, statePurged, stateRestored, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadTerminated, threadWaiting, vmInitialized

Methods inherited from class gov.nasa.jpf.GenericProperty

getErrorMessage, getExplanation, printOn

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, publishFinished, publishStart, publishTransition

Field Detail

trace

protected ChoiceGenerator<?>[] trace

showInsn

protected boolean showInsn

showLoc

protected boolean showLoc

showSrc

protected boolean showSrc

Constructor Detail

ErrorTraceGenerator

public ErrorTraceGenerator(Config conf,
                   JPF jpf)

Method Detail

publishPropertyViolation

public void publishPropertyViolation(Publisher p)

Specified by:

publishPropertyViolation in interface PublisherExtension

Overrides:

publishPropertyViolation in class PropertyListenerAdapter

propertyViolated

public void propertyViolated(Search search)

Description copied from interface: SearchListener

JPF encountered a property violation. Note - this is always preceeded by a stateAdvanced

Specified by:

propertyViolated in interface SearchListener

Overrides:

propertyViolated in class PropertyListenerAdapter