gov.nasa.jpf.symbc

Class SymbolicListener

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.symbc.SymbolicListener

All Implemented Interfaces:

gov.nasa.jpf.JPFListener, gov.nasa.jpf.Property, gov.nasa.jpf.report.PublisherExtension, gov.nasa.jpf.search.SearchListener, gov.nasa.jpf.util.Printable, gov.nasa.jpf.vm.VMListener, java.lang.Cloneable

public class SymbolicListener
extends gov.nasa.jpf.PropertyListenerAdapter
implements gov.nasa.jpf.report.PublisherExtension

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
protected class	SymbolicListener.MethodSummary

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<java.lang.String,SymbolicListener.MethodSummary>	allSummaries
private java.lang.String	currentMethodName

Constructor Summary

Constructors

Constructor and Description
SymbolicListener(gov.nasa.jpf.Config conf, gov.nasa.jpf.JPF jpf)

Method Summary

Modifier and Type	Method and Description
void	instructionExecuted(gov.nasa.jpf.vm.VM vm, gov.nasa.jpf.vm.ThreadInfo currentThread, gov.nasa.jpf.vm.Instruction nextInstruction, gov.nasa.jpf.vm.Instruction executedInstruction)
private void	printMethodSummary(java.io.PrintWriter pw, SymbolicListener.MethodSummary methodSummary)
private void	printMethodSummaryHTML(java.io.PrintWriter pw, SymbolicListener.MethodSummary methodSummary)
void	propertyViolated(gov.nasa.jpf.search.Search search)
void	publishFinished(gov.nasa.jpf.report.Publisher publisher)

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

check, choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, clone, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, loadClass, methodEntered, methodExited, objectCreated, objectExposed, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectShared, objectUnlocked, objectWait, publishConstraintHit, publishProbe, publishPropertyViolation, publishStart, publishTransition, reset, 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

getErrorMessage, getExplanation, printOn

Methods inherited from class java.lang.Object

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

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

publishConstraintHit, publishProbe, publishPropertyViolation, publishStart, publishTransition

Field Detail

allSummaries

private java.util.Map<java.lang.String,SymbolicListener.MethodSummary> allSummaries

currentMethodName

private java.lang.String currentMethodName

Constructor Detail

SymbolicListener

public SymbolicListener(gov.nasa.jpf.Config conf,
                        gov.nasa.jpf.JPF jpf)

Method Detail

propertyViolated

public void propertyViolated(gov.nasa.jpf.search.Search search)

Specified by:

propertyViolated in interface gov.nasa.jpf.search.SearchListener

Overrides:

propertyViolated in class gov.nasa.jpf.PropertyListenerAdapter

instructionExecuted

public void instructionExecuted(gov.nasa.jpf.vm.VM vm,
                                gov.nasa.jpf.vm.ThreadInfo currentThread,
                                gov.nasa.jpf.vm.Instruction nextInstruction,
                                gov.nasa.jpf.vm.Instruction executedInstruction)

Specified by:

instructionExecuted in interface gov.nasa.jpf.vm.VMListener

Overrides:

instructionExecuted in class gov.nasa.jpf.PropertyListenerAdapter

printMethodSummary

private void printMethodSummary(java.io.PrintWriter pw,
                                SymbolicListener.MethodSummary methodSummary)

printMethodSummaryHTML

private void printMethodSummaryHTML(java.io.PrintWriter pw,
                                    SymbolicListener.MethodSummary methodSummary)

publishFinished

public void publishFinished(gov.nasa.jpf.report.Publisher publisher)

Specified by:

publishFinished in interface gov.nasa.jpf.report.PublisherExtension

Overrides:

publishFinished in class gov.nasa.jpf.PropertyListenerAdapter