gov.nasa.jpf.vm

Class SingleProcessVM

java.lang.Object

gov.nasa.jpf.vm.VM

gov.nasa.jpf.vm.SingleProcessVM

public class SingleProcessVM
extends VM

Author:

Nastaran Shafiei Includes the VM initialization for executing single Java process To use this jpf.properties includes, vm.class = gov.nasa.jpf.vm.SingleProcessVM

Field Summary

Fields

Modifier and Type	Field and Description
protected ApplicationContext	appCtx

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

backtracker, CHECK_CONSISTENCY, config, EMPTY_ARGS, error_id, indentOutput, initialized, isBigEndian, isTraceReplay, lastTrailInfo, listeners, log, newStateId, out, path, pathOutput, postGcActions, restorer, runGc, serializer, ss, stateSet, timeModel, transitionOccurred, treeOutput, vm

Constructor Summary

Constructors

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

Method Summary

Methods

Modifier and Type	Method and Description
protected ApplicationContext	createApplicationContext()
ApplicationContext	getApplicationContext(int obj) given an object reference, it returns the ApplicationContext of the process to which this object belongs
ApplicationContext[]	getApplicationContexts()
int	getNumberOfApplications()
String	getSUTDescription()
String	getSUTName()
boolean	hasOnlyDaemonRunnablesOtherThan(ThreadInfo ti)
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.

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

activateGC, addListener, addPostGcAction, backtrack, breakTransition, checkConsistency, cleanUp, createMainThreadGroup, createMainThreadInfo, createMainThreadObject, createSystemClassLoaderInfo, createSystemClassLoaderObject, createThreadInfo, currentTimeMillis, dumpThreadStates, forceState, forward, getAliveThreadCount, getBacktracker, getChoiceGenerator, getChoiceGenerators, getChoiceGeneratorsOfType, getClassInfo, getClassLoader, getClassLoaderList, getClonedPath, getConfig, getCurrentChoiceGenerator, getCurrentThread, getCurrentTransition, getElementInfo, getException, getHeap, getInstruction, getJPF, getKernelState, getLastChoiceGeneratorOfType, getLastStep, getLastTransition, getLiveThreads, getMainClassInfo, getMainEntryMethodInfo, getModifiableElementInfo, getNextChoiceGenerator, getNextListenerOfType, getPath, getPathLength, getPendingException, getPendingOutput, getPlatformEndianness, getRestorableState, getRestorer, getRunnableThreadCount, getSchedulerFactory, getSerializer, getStartupSystemClassInfos, getStartupSystemClassNames, getStateCount, getStateId, getStateSet, getSystemState, getThreadList, getThreadName, getVM, handleException, hasListenerOfType, hasOtherNonDaemonRunnablesThan, hasOtherRunnablesThan, hasPendingException, hasToRecordPathOutput, hasToRecordSteps, ignoreState, ignoreState, initFields, initializeMainThread, initSubsystems, initSystemState, initTimeModel, isAtomic, 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, notifyObjectLocked, notifyObjectNotifies, notifyObjectNotifiesAll, notifyObjectReleased, notifyObjectUnlocked, notifyObjectWait, notifyThreadBlocked, notifyThreadInterrupted, notifyThreadNotified, notifyThreadScheduled, notifyThreadStarted, notifyThreadTerminated, notifyThreadWaiting, notifyVMInitialized, print, print, print, print, print, print, print, printCurrentStackTrace, printLiveThreadStatus, println, println, processPostGcActions, pushClinits, pushMainEntry, pushMainEntryArgs, recordSteps, registerClassLoader, registerThread, registerThreadListCleanup, removeListener, resetNextCG, restoreState, retainStateAttributes, setMandatoryNextChoiceGenerator, setNextChoiceGenerator, 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

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 String getSUTName()

Specified by:

getSUTName in class VM

getSUTDescription

public String getSUTDescription()

Specified by:

getSUTDescription in class VM

getApplicationContext

public ApplicationContext getApplicationContext(int obj)

Description copied from class: VM

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

Specified by:

getApplicationContext in class VM

getApplicationContexts

public ApplicationContext[] getApplicationContexts()

Specified by:

getApplicationContexts 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

hasOnlyDaemonRunnablesOtherThan

public boolean hasOnlyDaemonRunnablesOtherThan(ThreadInfo ti)

Specified by:

hasOnlyDaemonRunnablesOtherThan in class VM