| java.lang.Object
 gov.nasa.jpf.jvm.NativePeer
All known Subclasses: gov.nasa.jpf.jvm.JPF_java_io_PrintStream$,
| NativePeer | | public class NativePeer (Code) | | native peer classes are part of MJI and contain the code that is
executed by the host VM (i.e. outside the state-tracked JPF JVM). Each
class executed by JPF that has native mehods must have a native peer class
(which is looked up and associated at class loadtime)
|
| COND_DETERM_PREFIX | | final static String COND_DETERM_PREFIX(Code) | | |
| getGlobalPeerClassName | | static String getGlobalPeerClassName(String clsName)(Code) | | lookup the native peer as a global (i.e. no package) class. This is still
safe because the peer classname is fully qualified (has the model
package in it)
"user peer" classes are confined to what MJIEnv allows them to do
(no package required, since the target class package is mangled into
the name itself)
|
| getNativePeer | | static NativePeer getNativePeer(ClassInfo ci)(Code) | | this becomes the factory method to load either a plain (slow)
reflection-based peer (a NativePeer object), or some speed optimized
derived class object.
Watch out - this gets called before the ClassInfo is fully initialized
(we shouldn't rely on more than just its name here)
|
| getSystemPeerClassName | | static String getSystemPeerClassName(String clsName)(Code) | | "system peer" classes reside in gov...jvm, i.e. they can do
whatever JPF internal stuff they want to
|
| getUserPeerClassName | | static String getUserPeerClassName(String clsName)(Code) | | look up peer classes in same package like the model class. This is kind
of misleading since the model only gets seen by JPF, and the peer only
by the host VM, but it makes it easier to distribute if this is an
application specific combo. Otherwise the package of the native peer should
be chosen so that it can access the host VM classes it needs
|
| isMethodDeterministic | | boolean isMethodDeterministic(Method m)(Code) | | |
|
|