gov.nasa.jpf.vm

Class SingleProcessVM

java.lang.Object

gov.nasa.jpf.vm.VM

gov.nasa.jpf.vm.SingleProcessVM

public class SingleProcessVM
extends VM

Field Summary

Fields

Modifier and Type	Field and Description
protected ApplicationContext	appCtx
protected Predicate<ThreadInfo>	daemonRunnable
protected Predicate<ThreadInfo>	runnablePredicate

Fields inherited from class gov.nasa.jpf.vm.VM

alivePredicate, backtracker, CHECK_CONSISTENCY, config, EMPTY_ARGS, error_id, funcObjFactory, indentOutput, initialized, isBigEndian, isTraceReplay, jpf, lastTrailInfo, listeners, log, newStateId, out, path, pathOutput, postGcActions, processFinalizers, restorer, runGc, scheduler, serializer, ss, stateSet, timedoutRunnablePredicate, timeModel, transitionOccurred, treeOutput, userliveNonDaemonPredicate, userTimedoutRunnablePredicate, vm

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	SingleProcessVM()
	SingleProcessVM(JPF jpf, Config conf)

Method Summary

Modifier and Type	Method and Description
protected ApplicationContext	createApplicationContext()
ApplicationContext	getApplicationContext(int obj)
ApplicationContext[]	getApplicationContexts()
Predicate<ThreadInfo>	getAppTimedoutRunnablePredicate()
ApplicationContext	getCurrentApplicationContext() given an object reference, it returns the ApplicationContext of the process to which this object belongs
Predicate<ThreadInfo>	getDaemonRunnablePredicate()
java.util.Map<java.lang.Integer,IntTable<java.lang.String>>	getInitialInternStringsMap()
int	getNumberOfApplications()
Predicate<ThreadInfo>	getRunnablePredicate()
java.lang.String	getSUTDescription()
java.lang.String	getSUTName()
boolean	initialize() this is the main initialization point that sets up startup objects threads and callstacks.
boolean	isDeadlocked()
boolean	isEndState() The program is terminated if there are no alive threads, and there is no nonDaemon left.
void	terminateProcess(ThreadInfo ti)

Methods inherited from class gov.nasa.jpf.vm.VM

activateGC, addListener, addPostGcAction, backtrack, breakTransition, checkConsistency, cleanUp, createFinalizerThreadInfo, createMainThreadInfo, createSystemClassLoaderInfo, createSystemClassLoaderObject, createThreadInfo, currentTimeMillis, dumpThreadStates, finalizersEnabled, forceState, forward, getAlivePredicate, getBacktracker, getChoiceGenerator, getChoiceGenerators, getChoiceGeneratorsOfType, getClassInfo, getClassLoader, getClassLoaderList, getClonedPath, getConfig, getCurrentChoiceGenerator, getCurrentThread, getCurrentTransition, getElementInfo, getException, getFinalizerThread, getFunctionObjectFacotry, getHeap, getInstruction, getJPF, getKernelState, getLastChoiceGeneratorInThread, getLastChoiceGeneratorOfType, getLastStep, getLastTransition, getLiveThreads, getMainClassInfo, getMainEntryMethodInfo, getModifiableElementInfo, getNextChoiceGenerator, getNextListenerOfType, getPath, getPathLength, getPendingException, getPendingOutput, getPlatformEndianness, getRestorableState, getRestorer, getScheduler, getSearch, getSerializer, getStartupSystemClassInfos, getStartupSystemClassNames, getStateCount, getStateId, getStateSet, getSystemState, getThreadList, getThreadName, getTimedoutRunnablePredicate, getUserLiveNonDaemonPredicate, getUserTimedoutRunnablePredicate, getVM, handleException, hasListenerOfType, hasNextChoiceGenerator, hasPendingException, hasToRecordPathOutput, hasToRecordSteps, ignoreState, ignoreState, initFields, initializeFinalizerThread, initializeMainThread, initSubsystems, initSystemState, initTimeModel, isBigEndianPlatform, isBoringState, isIgnoredState, isInitialized, isInterestingState, isNewState, isSingleProcess, isTraceReplay, isVisitedState, kernelStateChanged, nanoTime, notifyChoiceGeneratorAdvanced, notifyChoiceGeneratorProcessed, notifyChoiceGeneratorRegistered, notifyChoiceGeneratorSet, notifyClassLoaded, notifyExceptionBailout, notifyExceptionHandled, notifyExceptionThrown, notifyExecuteInstruction, notifyGCBegin, notifyGCEnd, notifyInstructionExecuted, notifyLoadClass, notifyMethodEntered, notifyMethodExited, notifyObjectCreated, notifyObjectExposed, notifyObjectLocked, notifyObjectNotifies, notifyObjectNotifiesAll, notifyObjectReleased, notifyObjectShared, notifyObjectUnlocked, notifyObjectWait, notifyThreadBlocked, notifyThreadInterrupted, notifyThreadNotified, notifyThreadScheduled, notifyThreadStarted, notifyThreadTerminated, notifyThreadWaiting, notifyVMInitialized, print, print, print, print, print, print, print, printChoiceGeneratorStack, printCurrentStackTrace, printLiveThreadStatus, println, println, processFinalizers, processPostGcActions, pushClinits, pushMainEntry, pushMainEntryArgs, recordSteps, registerClassLoader, registerThread, registerThreadListCleanup, removeListener, resetNextCG, restoreState, retainStateAttributes, setMandatoryNextChoiceGenerator, setNextChoiceGenerator, setRootCG, setSerializer, setTraceReplay, storePathOutput, storeTrace, transitionOccurred, updatePath

Methods inherited from class java.lang.Object

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

Field Detail

appCtx

protected ApplicationContext appCtx

runnablePredicate

protected Predicate<ThreadInfo> runnablePredicate

daemonRunnable

protected Predicate<ThreadInfo> daemonRunnable

Constructor Detail

SingleProcessVM

protected SingleProcessVM()

SingleProcessVM

public SingleProcessVM(JPF jpf,
                       Config conf)

Method Detail

createApplicationContext

protected ApplicationContext createApplicationContext()

initialize

public boolean initialize()

Description copied from class: VM

this is the main initialization point that sets up startup objects threads and callstacks. If this returns false VM initialization cannot proceed and JPF will terminate

Specified by:

initialize in class VM

getNumberOfApplications

public int getNumberOfApplications()

Specified by:

getNumberOfApplications in class VM

getSUTName

public java.lang.String getSUTName()

Specified by:

getSUTName in class VM

getSUTDescription

public java.lang.String getSUTDescription()

Specified by:

getSUTDescription in class VM

getApplicationContext

public ApplicationContext getApplicationContext(int obj)

Specified by:

getApplicationContext in class VM

getApplicationContexts

public ApplicationContext[] getApplicationContexts()

Specified by:

getApplicationContexts in class VM

getCurrentApplicationContext

public ApplicationContext getCurrentApplicationContext()

Description copied from class: VM

given an object reference, it returns the ApplicationContext of the process to which this object belongs

Specified by:

getCurrentApplicationContext in class VM

isEndState

public boolean isEndState()

The program is terminated if there are no alive threads, and there is no nonDaemon left. NOTE - this is only approximated in real life. Daemon threads can still run for a few cycles after the last non-daemon died, which opens an interesting source of errors we actually might want to check for

Specified by:

isEndState in class VM

isDeadlocked

public boolean isDeadlocked()

Specified by:

isDeadlocked in class VM

terminateProcess

public void terminateProcess(ThreadInfo ti)

Specified by:

terminateProcess in class VM

getInitialInternStringsMap

public java.util.Map<java.lang.Integer,IntTable<java.lang.String>> getInitialInternStringsMap()

Specified by:

getInitialInternStringsMap in class VM

getRunnablePredicate

public Predicate<ThreadInfo> getRunnablePredicate()

Specified by:

getRunnablePredicate in class VM

getAppTimedoutRunnablePredicate

public Predicate<ThreadInfo> getAppTimedoutRunnablePredicate()

Specified by:

getAppTimedoutRunnablePredicate in class VM

getDaemonRunnablePredicate

public Predicate<ThreadInfo> getDaemonRunnablePredicate()

Specified by:

getDaemonRunnablePredicate in class VM