001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package java.lang;
020:
021: import gov.nasa.jpf.JPFException;
022:
023: import java.io.InputStream;
024: import java.lang.reflect.Field;
025: import java.lang.reflect.Method;
026: import java.lang.reflect.Constructor;
027: import java.net.URL;
028:
029: /**
030: * MJI model class for java.lang.Class library abstraction
031: *
032: * This is a JPF specific version of a system class because we can't use the real,
033: * platform JVM specific version (it's native all over the place, its field
034: * structure isn't documented, most of its methods are private, hence we can't
035: * even instantiate it properly).
036: *
037: * Note that this class never gets seen by the real VM - it's for JPF's eyes only.
038: *
039: * For now, it's only a fragment to test the mechanism, and provide basic
040: * class.getName() / Class.ForName() support (which is (almost) enough for
041: * Java assertion support
042: */
043: public class Class {
044: private String name;
045:
046: /**
047: * this is the StaticArea ref of the class we refer to
048: * (so that we don't have to convert to a Java String in the peer all the time)
049: */
050: private int cref;
051:
052: /**
053: * to be set during <clinit> of the corresponding class
054: */
055: private boolean isPrimitive;
056:
057: public native boolean isArray();
058:
059: public native Class getComponentType();
060:
061: public Field getDeclaredField(String fieldName)
062: throws NoSuchFieldException, SecurityException {
063: // <2do>
064: throw new JPFException(
065: "Class.getDeclaredField() not yet supported");
066: }
067:
068: public Method getDeclaredMethod(String mthName, Class[] paramTypes)
069: throws NoSuchMethodException, SecurityException {
070: // <2do>
071: throw new JPFException(
072: "Class.getDeclaredMethod() not yet supported");
073: }
074:
075: public InputStream getResourceAsStream(String name) {
076: throw new JPFException(
077: "Class.getResourceAsStream() not yet supported");
078: }
079:
080: public URL getResource(String name) {
081: throw new JPFException("Class.getResource() not yet supported");
082: }
083:
084: public Constructor getDeclaredConstructor(Class[] paramTypes)
085: throws NoSuchMethodException, SecurityException {
086: // <2do>
087: throw new JPFException(
088: "Class.getDeclaredConstructor() not yet supported");
089: }
090:
091: public Method[] getDeclaredMethods() throws SecurityException {
092: // <2do>
093: throw new JPFException(
094: "Class.getDeclaredMethods() not yet supported");
095: }
096:
097: public Field getField(String fieldName)
098: throws NoSuchFieldException, SecurityException {
099: // <2do>
100: throw new JPFException("Class.getField() not yet supported");
101: }
102:
103: public native boolean isInstance(Object o);
104:
105: public native boolean isAssignableFrom(Class clazz);
106:
107: public Method getMethod(String mthName, Class[] paramTypes)
108: throws NoSuchMethodException, SecurityException {
109: // <2do>
110: throw new JPFException("Class.getMethod() not yet supported");
111: }
112:
113: public Constructor getConstructor(Class[] argTypes)
114: throws NoSuchMethodException {
115: throw new JPFException(
116: "Class.getConstructor() not yet supported");
117: }
118:
119: // no use to have a ctor, we can't call it
120: public String getName() {
121: return name;
122: }
123:
124: public static native Class getPrimitiveClass(String clsName);
125:
126: /**
127: * this one is in JPF reflection land, it's 'native' for us
128: */
129: public static native Class forName(String clsName)
130: throws ClassNotFoundException;
131:
132: public boolean isPrimitive() {
133: return isPrimitive;
134: }
135:
136: public native Class getSuperclass();
137:
138: public native Object newInstance() throws InstantiationException,
139: IllegalAccessException;
140:
141: public String toString() {
142: return ("class " + name);
143: }
144:
145: native boolean desiredAssertionStatus();
146: }
|