|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectgov.nasa.jpf.GenericProperty
gov.nasa.jpf.PropertyListenerAdapter
org.objectweb.dsrg.sofa.cushion.jpfcheck.ProtocolListener
public class ProtocolListener
Listener for JPF that monitors protocol-related events (method invoke and return) and notifies the BPChecker when any such event occurs.
Constructor Summary | |
---|---|
ProtocolListener(org.ow2.dsrg.fm.origbp.DFSR.JPFTraverser tr,
java.util.Map itf2class,
java.util.Set serverItfs,
java.lang.String[] events)
|
Method Summary | |
---|---|
java.lang.String |
getErrorMessage()
|
java.util.Set |
getMethodNames()
Returns names of methods that are monitored by JPF. |
boolean |
check(gov.nasa.jpf.search.Search search,
gov.nasa.jpf.jvm.JVM vm)
|
void |
instructionExecuted(gov.nasa.jpf.jvm.JVM vm)
|
void |
searchFinished(gov.nasa.jpf.search.Search search)
|
void |
stateAdvanced(gov.nasa.jpf.search.Search search)
|
void |
stateBacktracked(gov.nasa.jpf.search.Search search)
|
void |
stateProcessed(gov.nasa.jpf.search.Search search)
|
Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter |
---|
classLoaded, exceptionThrown, executeInstruction, gcBegin, gcEnd, choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorSet, objectCreated, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectUnlocked, objectWait, propertyViolated, publishFinished, publishPropertyViolation, publishStart, publishTransition, searchConstraintHit, searchStarted, stateRestored, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadTerminated, threadWaiting |
Methods inherited from class gov.nasa.jpf.GenericProperty |
---|
getExplanation, printOn, reset |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
---|
public ProtocolListener(org.ow2.dsrg.fm.origbp.DFSR.JPFTraverser tr, java.util.Map itf2class, java.util.Set serverItfs, java.lang.String[] events)
itf2class
- map of names of interfaces to names of classes that implement them.serverItfs
- list of names of fractal server interfaces.events
- list of events that should be passed to the BP checker.Method Detail |
---|
public java.util.Set getMethodNames()
public void stateAdvanced(gov.nasa.jpf.search.Search search)
stateAdvanced
in interface gov.nasa.jpf.search.SearchListener
stateAdvanced
in class gov.nasa.jpf.PropertyListenerAdapter
public void stateBacktracked(gov.nasa.jpf.search.Search search)
stateBacktracked
in interface gov.nasa.jpf.search.SearchListener
stateBacktracked
in class gov.nasa.jpf.PropertyListenerAdapter
public void stateProcessed(gov.nasa.jpf.search.Search search)
stateProcessed
in interface gov.nasa.jpf.search.SearchListener
stateProcessed
in class gov.nasa.jpf.PropertyListenerAdapter
public void searchFinished(gov.nasa.jpf.search.Search search)
searchFinished
in interface gov.nasa.jpf.search.SearchListener
searchFinished
in class gov.nasa.jpf.PropertyListenerAdapter
public void instructionExecuted(gov.nasa.jpf.jvm.JVM vm)
instructionExecuted
in interface gov.nasa.jpf.jvm.VMListener
instructionExecuted
in class gov.nasa.jpf.PropertyListenerAdapter
public boolean check(gov.nasa.jpf.search.Search search, gov.nasa.jpf.jvm.JVM vm)
check
in interface gov.nasa.jpf.Property
check
in class gov.nasa.jpf.PropertyListenerAdapter
public java.lang.String getErrorMessage()
getErrorMessage
in interface gov.nasa.jpf.Property
getErrorMessage
in class gov.nasa.jpf.GenericProperty
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |