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 gov.nasa.jpf.jvm;
020:
021: import gov.nasa.jpf.JPFException;
022: import gov.nasa.jpf.jvm.bytecode.Instruction;
023:
024: /**
025: * NativePeerDispatcher example (generated by GenPeerDispatcher)
026: */
027: class JPF_java_io_PrintStream$ extends NativePeer {
028: boolean isMethodCondDeterministic(ThreadInfo ti, MethodInfo mi) {
029: boolean ret = false;
030: int mid = mi.getUniqueName().hashCode();
031:
032: MJIEnv env = ti.getMJIEnv();
033: int rThis = (mi.isStatic()) ? ci.getClassObjectRef() : ti
034: .getCalleeThis(mi);
035:
036: env.setCallEnvironment(mi);
037:
038: try {
039: switch (mid) {
040: default:
041: throw new JPFException(
042: "no isDeterministic() condition: "
043: + mi.getName());
044: }
045: } catch (Throwable x) {
046: x.printStackTrace();
047: }
048:
049: return ret;
050: }
051:
052: boolean isMethodCondExecutable(ThreadInfo ti, MethodInfo mi) {
053: boolean ret = false;
054: int mid = mi.getUniqueName().hashCode();
055:
056: MJIEnv env = ti.getMJIEnv();
057: int rThis = (mi.isStatic()) ? ci.getClassObjectRef() : ti
058: .getCalleeThis(mi);
059:
060: env.setCallEnvironment(mi);
061:
062: try {
063: switch (mid) {
064: default:
065: throw new JPFException("no isExecutable() condition: "
066: + mi.getName());
067: }
068: } catch (Throwable x) {
069: x.printStackTrace();
070: }
071:
072: return ret;
073: }
074:
075: Instruction executeMethod(ThreadInfo ti, MethodInfo mi) {
076: int iret = 0;
077: long lret = 0;
078: int retSize = 0;
079: String exception = null;
080: int mid = mi.getUniqueName().hashCode();
081:
082: MJIEnv env = ti.getMJIEnv();
083: int rThis = (mi.isStatic()) ? ci.getClassObjectRef() : ti
084: .getCalleeThis(mi);
085: env.setCallEnvironment(mi);
086:
087: try {
088: switch (mid) {
089: case -1796256208: // println()
090: retSize = 0;
091: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.println__(env,
092: rThis);
093:
094: break;
095:
096: case 628854628: // print(Ljava/lang/String;)
097: retSize = 0;
098: gov.nasa.jpf.jvm.JPF_java_io_PrintStream
099: .print__Ljava_lang_String_2(env, rThis, ti
100: .peek(0));
101:
102: break;
103:
104: case 1440870566: // println(Ljava/lang/String;)
105: retSize = 0;
106: gov.nasa.jpf.jvm.JPF_java_io_PrintStream
107: .println__Ljava_lang_String_2(env, rThis, ti
108: .peek(0));
109:
110: break;
111:
112: case -1166388901: // print(I)
113: retSize = 0;
114: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.print__I(env,
115: rThis, ti.peek(0));
116:
117: break;
118:
119: case 150633433: // println(I)
120: retSize = 0;
121: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.println__I(
122: env, rThis, ti.peek(0));
123:
124: break;
125:
126: case -1166388994: // print(F)
127: retSize = 0;
128: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.print__F(env,
129: rThis, Types.intToFloat(ti.peek(0)));
130:
131: break;
132:
133: case 150633340: // println(F)
134: retSize = 0;
135: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.println__F(
136: env, rThis, Types.intToFloat(ti.peek(0)));
137:
138: break;
139:
140: case -1166388870: // print(J)
141: retSize = 0;
142: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.print__J(env,
143: rThis, ti.longPeek(0));
144:
145: break;
146:
147: case 150633464: // println(J)
148: retSize = 0;
149: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.println__J(
150: env, rThis, ti.longPeek(0));
151:
152: break;
153:
154: case -1166389056: // print(D)
155: retSize = 0;
156: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.print__D(env,
157: rThis, Types.longToDouble(ti.longPeek(0)));
158:
159: break;
160:
161: case 150633278: // println(D)
162: retSize = 0;
163: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.println__D(
164: env, rThis, Types.longToDouble(ti.longPeek(0)));
165:
166: break;
167:
168: case -1166388374: // print(Z)
169: retSize = 0;
170: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.print__Z(env,
171: rThis, Types.intToBoolean(ti.peek(0)));
172:
173: break;
174:
175: case 150633960: // println(Z)
176: retSize = 0;
177: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.println__Z(
178: env, rThis, Types.intToBoolean(ti.peek(0)));
179:
180: break;
181:
182: case 150633247: // println(C)
183: retSize = 0;
184: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.println__C(
185: env, rThis, (char) ti.peek(0));
186:
187: break;
188:
189: case -1166389087: // print(C)
190: retSize = 0;
191: gov.nasa.jpf.jvm.JPF_java_io_PrintStream.print__C(env,
192: rThis, (char) ti.peek(0));
193:
194: break;
195:
196: case 754558870: // write(Ljava/lang/String;)
197: retSize = 0;
198: gov.nasa.jpf.jvm.JPF_java_io_PrintStream
199: .write__Ljava_lang_String_2(env, rThis, ti
200: .peek(0));
201:
202: break;
203:
204: default:
205: return ti.createAndThrowException(
206: "java.lang.UnsatisfiedLinkError",
207: "cannot find: " + ci.getName() + '.'
208: + mi.getName());
209: }
210: } catch (Throwable x) {
211: x.printStackTrace();
212:
213: return ti.createAndThrowException(
214: "java.lang.reflect.InvocationTargetException", ci
215: .getName()
216: + '.' + mi.getName());
217: }
218:
219: if ((exception = env.getException()) != null) {
220: return ti.createAndThrowException(exception);
221: }
222:
223: if (env.getRepeat()) {
224: return ti.getPC();
225: }
226:
227: ti.removeArguments(mi);
228:
229: switch (retSize) {
230: case 0:
231: break; // nothing to return
232:
233: case 1:
234: ti.push(iret, mi.isReferenceReturnType());
235:
236: break;
237:
238: case 2:
239: ti.longPush(lret);
240:
241: break;
242: }
243:
244: return ti.getPC().getNext();
245: }
246: }
|