gov.nasa.jpf.listener

Class AssertionProperty

java.lang.Object

gov.nasa.jpf.GenericProperty

gov.nasa.jpf.PropertyListenerAdapter

gov.nasa.jpf.listener.AssertionProperty

All Implemented Interfaces:

JPFListener, Property, PublisherExtension, SearchListener, Printable, VMListener

public class AssertionProperty
extends PropertyListenerAdapter

this is a property listener that turns thrown AssertionErrors into property violations before they are caught (i.e. potentially change the stack). Besides serving the purpose of eliminating the "catch(Throwable)" case, it can be used in conjunction with "search.multiple_errors=true" to report assertions but otherwise ignore them and go on searching the same path (otherwise, multiple_errors would cause a backtrack)

Constructor Summary

Constructors

Constructor and Description
AssertionProperty(Config config)

Method Summary

Methods

Modifier and Type	Method and Description
boolean	check(Search search, VM vm) return true if property is NOT violated
void	executeInstruction(VM vm, ThreadInfo ti, Instruction insn) VM is about to execute the next instruction
String	getErrorMessage()
protected String	getMessage(String details, Instruction insn)
void	reset()

Methods inherited from class gov.nasa.jpf.PropertyListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, exceptionBailout, exceptionHandled, exceptionThrown, gcBegin, gcEnd, instructionExecuted, loadClass, methodEntered, methodExited, objectCreated, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, publishFinished, publishPropertyViolation, publishStart, publishTransition, 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

getExplanation, printOn

Methods inherited from class java.lang.Object

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

Constructor Detail

AssertionProperty

public AssertionProperty(Config config)

Method Detail

check

public boolean check(Search search,
            VM vm)

Description copied from interface: Property

return true if property is NOT violated

Specified by:

check in interface Property

Overrides:

check in class PropertyListenerAdapter

getErrorMessage

public String getErrorMessage()

Specified by:

getErrorMessage in interface Property

Overrides:

getErrorMessage in class GenericProperty

getMessage

protected String getMessage(String details,
                Instruction insn)

executeInstruction

public void executeInstruction(VM vm,
                      ThreadInfo ti,
                      Instruction insn)

Description copied from interface: VMListener

VM is about to execute the next instruction

Specified by:

executeInstruction in interface VMListener

Overrides:

executeInstruction in class PropertyListenerAdapter

reset

public void reset()

Specified by:

reset in interface Property

Overrides:

reset in class PropertyListenerAdapter