gov.nasa.jpf.symbc

Class SymbolicListener2

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.symbc.SymbolicListener2

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 SymbolicListener2
extends gov.nasa.jpf.PropertyListenerAdapter

Field Summary

Fields

Modifier and Type	Field and Description
(package private) java.util.concurrent.BlockingQueue<gov.nasa.jpf.util.Pair<gov.nasa.jpf.symbc.numeric.PathCondition,java.util.Map<java.lang.String,java.lang.Object>>>	pcAndSolutionQueue
private java.lang.String	targetMethodName

Constructor Summary

Constructors

Constructor and Description
SymbolicListener2(gov.nasa.jpf.Config conf, gov.nasa.jpf.JPF jpf, java.util.concurrent.BlockingQueue<gov.nasa.jpf.util.Pair<gov.nasa.jpf.symbc.numeric.PathCondition,java.util.Map<java.lang.String,java.lang.Object>>> pcAndSolutionQueue)

Method Summary

Modifier and Type	Method and Description
private void	handleNewPathCondition(gov.nasa.jpf.symbc.numeric.PathCondition pc)
void	methodExited(gov.nasa.jpf.vm.VM vm, gov.nasa.jpf.vm.ThreadInfo currentThread, gov.nasa.jpf.vm.MethodInfo exitedMethod)
void	propertyViolated(gov.nasa.jpf.search.Search search)

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

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

Field Detail

pcAndSolutionQueue

java.util.concurrent.BlockingQueue<gov.nasa.jpf.util.Pair<gov.nasa.jpf.symbc.numeric.PathCondition,java.util.Map<java.lang.String,java.lang.Object>>> pcAndSolutionQueue

targetMethodName

private java.lang.String targetMethodName

Constructor Detail

SymbolicListener2

public SymbolicListener2(gov.nasa.jpf.Config conf,
                         gov.nasa.jpf.JPF jpf,
                         java.util.concurrent.BlockingQueue<gov.nasa.jpf.util.Pair<gov.nasa.jpf.symbc.numeric.PathCondition,java.util.Map<java.lang.String,java.lang.Object>>> pcAndSolutionQueue)

Method Detail

methodExited

public void methodExited(gov.nasa.jpf.vm.VM vm,
                         gov.nasa.jpf.vm.ThreadInfo currentThread,
                         gov.nasa.jpf.vm.MethodInfo exitedMethod)

Specified by:

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

Overrides:

methodExited in class gov.nasa.jpf.PropertyListenerAdapter

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

handleNewPathCondition

private void handleNewPathCondition(gov.nasa.jpf.symbc.numeric.PathCondition pc)