gov.nasa.jpf.jvm

Class JVMSystemClassLoaderInfo

java.lang.Object

gov.nasa.jpf.vm.ClassLoaderInfo

gov.nasa.jpf.vm.SystemClassLoaderInfo

gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo

All Implemented Interfaces:

Restorable<ClassLoaderInfo>, java.lang.Cloneable, java.lang.Comparable<ClassLoaderInfo>, java.lang.Iterable<ClassInfo>

public class JVMSystemClassLoaderInfo
extends SystemClassLoaderInfo

a SystemClassLoaderInfo that reads standard Java classfiles from *.class and *.jar files, and creates code using a concrete value JVM instruction set

Field Summary

Fields

Modifier and Type	Field and Description
protected JVMCodeBuilder	defaultCodeBuilder

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

attributors, charArrayClassInfo, classClassInfo, classLoaderClassInfo, enumClassInfo, objectClassInfo, refClassInfo, stringClassInfo, threadClassInfo, threadGroupClassInfo, unCachedClasses, weakRefClassInfo

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

classAssertionStatus, classInfo, config, cp, defaultAssertionStatus, globalCLids, id, ID_FIELD, isDefaultSet, loadedAnnotations, loadedClasses, objRef, packageAssertionStatus, parent, resolvedAnnotations, resolvedClasses, roundTripRequired, statics

Constructor Summary

Constructors

Constructor and Description
JVMSystemClassLoaderInfo(VM vm, int appId)

Method Summary

Modifier and Type	Method and Description
protected void	addSystemBootClassPath()
protected ClassFileContainer	createClassFileContainer(java.lang.String spec)
protected ClassInfo	createClassInfo(java.lang.String clsName, java.lang.String url, byte[] data, ClassLoaderInfo definingLoader)
protected JVMCodeBuilder	createDefaultCodeBuilder(Config config, int appId) override this if you need a different default CodeBuilder
protected JVMCodeBuilder	getCodeBuilder(java.lang.String clsName) override this if you have different CodeBuilders for different types NOTE - this CodeBuilder is not completely initialized yet, clients still have to call startMethod(mi) on it
protected JVMCodeBuilder	getSystemCodeBuilder(ClassFile cf, MethodInfo mi) used for automatically created code such as AnnotationProxies, direct calls, native calls and run starts NOTE - this cannot be called recursively or concurrently
protected void	initializeSystemClassPath(VM vm, int appId) this is the main method to create the ClassPath, which is called from the ctor

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

addAttributor, getCharArrayClassInfo, getClassClassInfo, getClassLoaderClassInfo, getEnumClassInfo, getObjectClassInfo, getPathElements, getReferenceClassInfo, getResolvedClassInfo, getStringClassInfo, getSystemClassLoader, getThreadClassInfo, getThreadGroupClassInfo, getWeakReferenceClassInfo, initializeAttributors, isSystemClassLoader, loadClass, loadSystemClass, setAttributes, setClassLoaderObject, updateCachedClassInfos

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

addClassPathElement, addResolvedClass, clearAssertionStatus, compareTo, computeId, createClassInfo, createStatics, desiredAssertionStatus, findResource, findResources, getAlreadyResolvedClassInfo, getClassInfo, getClassInfo, getClassLoaderObjectRef, getClassPath, getClassPathElements, getCurrentClassLoader, getCurrentClassLoader, getCurrentResolvedClassInfo, getCurrentSystemClassLoader, getDefinedClassInfo, getElementInfo, getId, getInitializedClassInfo, getMatch, getMemento, getMemento, getModifiableElementInfo, getNumberOfLoadedClasses, getPackages, getResolvedAnnotationInfo, getResolvedAnnotationProxy, getResolvedClassInfo, getResolvedFuncObjType, getResourceURL, getStatics, getSystemResolvedClassInfo, hasResolved, isAlive, isRoundTripRequired, iterator, loadClassOnJPF, loadClassOnJVM, pushloadClassFrame, setClassAssertionStatus, setDefaultAssertionStatus, setPackageAssertionStatus, tryGetResolvedClassInfo

Methods inherited from class java.lang.Object

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

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

defaultCodeBuilder

protected JVMCodeBuilder defaultCodeBuilder

Constructor Detail

JVMSystemClassLoaderInfo

public JVMSystemClassLoaderInfo(VM vm,
                                int appId)

Method Detail

createDefaultCodeBuilder

protected JVMCodeBuilder createDefaultCodeBuilder(Config config,
                                                  int appId)

override this if you need a different default CodeBuilder

createClassFileContainer

protected ClassFileContainer createClassFileContainer(java.lang.String spec)

Overrides:

createClassFileContainer in class ClassLoaderInfo

addSystemBootClassPath

protected void addSystemBootClassPath()

initializeSystemClassPath

protected void initializeSystemClassPath(VM vm,
                                         int appId)

this is the main method to create the ClassPath, which is called from the ctor

Specified by:

initializeSystemClassPath in class SystemClassLoaderInfo

getCodeBuilder

protected JVMCodeBuilder getCodeBuilder(java.lang.String clsName)

override this if you have different CodeBuilders for different types NOTE - this CodeBuilder is not completely initialized yet, clients still have to call startMethod(mi) on it

getSystemCodeBuilder

protected JVMCodeBuilder getSystemCodeBuilder(ClassFile cf,
                                              MethodInfo mi)

used for automatically created code such as AnnotationProxies, direct calls, native calls and run starts NOTE - this cannot be called recursively or concurrently

createClassInfo

protected ClassInfo createClassInfo(java.lang.String clsName,
                                    java.lang.String url,
                                    byte[] data,
                                    ClassLoaderInfo definingLoader)
                             throws ClassParseException

Overrides:

createClassInfo in class ClassLoaderInfo

Throws:

ClassParseException