gov.nasa.jpf.util

Class TypeRef

java.lang.Object

gov.nasa.jpf.util.TypeRef

public class TypeRef
extends java.lang.Object

this is a utility construct for type references that should not cause class loading when instantiated, but cannot use a classname String because of argument type ambiguity (Strings are just used everywhere). TypeRefs can be used to specify both native and JPF executed (SUT) classes, it is up to the caller to use the proper access methods NOTE - loading and instantiation of TypeRefs is not allowed to cause loading of any JPF classes that are not in jpf-classes.jar

Constructor Summary

Constructors

Constructor and Description
TypeRef(java.lang.String clsName)

Method Summary

Modifier and Type	Method and Description
<T> java.lang.Class<? extends T>	asNativeSubclass(java.lang.Class<T> superClazz) return the host VM class for this ref.
ClassInfo	getClassInfo() obtain the ClassInfo (JPF class) for this ref.
java.lang.Class<?>	getNativeClass()
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Constructor Detail

TypeRef

public TypeRef(java.lang.String clsName)

Method Detail

getNativeClass

public java.lang.Class<?> getNativeClass()
                                  throws java.lang.ClassNotFoundException

Throws:

java.lang.ClassNotFoundException

asNativeSubclass

public <T> java.lang.Class<? extends T> asNativeSubclass(java.lang.Class<T> superClazz)
                                                  throws java.lang.ClassNotFoundException,
                                                         java.lang.ClassCastException

return the host VM class for this ref. This will cause native on-demand class loading

Throws:

java.lang.ClassNotFoundException

java.lang.ClassCastException

getClassInfo

public ClassInfo getClassInfo()

obtain the ClassInfo (JPF class) for this ref. This will cause on-demand class loading by JPF

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object