01: package de.uka.ilkd.key.javacard;
02:
03: /** This class contains methods specific to KeY model of the Java Card
04: * API (2.1.1 & 2.2.1). These methods do not have any specs as they
05: * should be always symbolically executed in the proof with dedicated
06: * taclets. No contracts should be used for these methods (especially
07: * the jvm*Transaction methods).
08: */
09: public class KeYJCSystem {
10:
11: public static native byte jvmIsTransient(Object theObj);
12:
13: public static native boolean[] jvmMakeTransientBooleanArray(
14: short length, byte event);
15:
16: public static native byte[] jvmMakeTransientByteArray(short length,
17: byte event);
18:
19: public static native short[] jvmMakeTransientShortArray(
20: short length, byte event);
21:
22: public static native Object[] jvmMakeTransientObjectArray(
23: short length, byte event);
24:
25: public final static native void jvmBeginTransaction();
26:
27: public static native void jvmAbortTransaction();
28:
29: public static native void jvmCommitTransaction();
30:
31: public static native void jvmSuspendTransaction();
32:
33: public static native void jvmResumeTransaction();
34:
35: public static native void jvmArrayCopy(byte[] src, short srcOff,
36: byte[] dest, short destOff, short length);
37:
38: public static native void jvmArrayCopyNonAtomic(byte[] src,
39: short srcOff, byte[] dest, short destOff, short length);
40:
41: public static native void jvmArrayFillNonAtomic(byte[] bArray,
42: short bOff, short bLen, byte bValue);
43:
44: public static native byte jvmArrayCompare(byte[] src, short srcOff,
45: byte[] dest, short destOff, short length);
46:
47: public static native short jvmMakeShort(byte b1, byte b2);
48:
49: public static native short jvmSetShort(byte[] bArray, short bOff,
50: short sValue);
51:
52: }
|