| java.lang.Object de.uka.ilkd.key.javacard.KeYJCSystem
KeYJCSystem | public class KeYJCSystem (Code) | | This class contains methods specific to KeY model of the Java Card
API (2.1.1 & 2.2.1). These methods do not have any specs as they
should be always symbolically executed in the proof with dedicated
taclets. No contracts should be used for these methods (especially
the jvm*Transaction methods).
|
Method Summary | |
native public static void | jvmAbortTransaction() | native public static byte | jvmArrayCompare(byte[] src, short srcOff, byte[] dest, short destOff, short length) | native public static void | jvmArrayCopy(byte[] src, short srcOff, byte[] dest, short destOff, short length) | native public static void | jvmArrayCopyNonAtomic(byte[] src, short srcOff, byte[] dest, short destOff, short length) | native public static void | jvmArrayFillNonAtomic(byte[] bArray, short bOff, short bLen, byte bValue) | final native public static void | jvmBeginTransaction() | native public static void | jvmCommitTransaction() | native public static byte | jvmIsTransient(Object theObj) | native public static short | jvmMakeShort(byte b1, byte b2) | native public static boolean[] | jvmMakeTransientBooleanArray(short length, byte event) | native public static byte[] | jvmMakeTransientByteArray(short length, byte event) | native public static Object[] | jvmMakeTransientObjectArray(short length, byte event) | native public static short[] | jvmMakeTransientShortArray(short length, byte event) | native public static void | jvmResumeTransaction() | native public static short | jvmSetShort(byte[] bArray, short bOff, short sValue) | native public static void | jvmSuspendTransaction() |
jvmAbortTransaction | native public static void jvmAbortTransaction()(Code) | | |
jvmArrayCompare | native public static byte jvmArrayCompare(byte[] src, short srcOff, byte[] dest, short destOff, short length)(Code) | | |
jvmArrayCopy | native public static void jvmArrayCopy(byte[] src, short srcOff, byte[] dest, short destOff, short length)(Code) | | |
jvmArrayCopyNonAtomic | native public static void jvmArrayCopyNonAtomic(byte[] src, short srcOff, byte[] dest, short destOff, short length)(Code) | | |
jvmArrayFillNonAtomic | native public static void jvmArrayFillNonAtomic(byte[] bArray, short bOff, short bLen, byte bValue)(Code) | | |
jvmBeginTransaction | final native public static void jvmBeginTransaction()(Code) | | |
jvmCommitTransaction | native public static void jvmCommitTransaction()(Code) | | |
jvmIsTransient | native public static byte jvmIsTransient(Object theObj)(Code) | | |
jvmMakeShort | native public static short jvmMakeShort(byte b1, byte b2)(Code) | | |
jvmMakeTransientBooleanArray | native public static boolean[] jvmMakeTransientBooleanArray(short length, byte event)(Code) | | |
jvmMakeTransientByteArray | native public static byte[] jvmMakeTransientByteArray(short length, byte event)(Code) | | |
jvmMakeTransientObjectArray | native public static Object[] jvmMakeTransientObjectArray(short length, byte event)(Code) | | |
jvmMakeTransientShortArray | native public static short[] jvmMakeTransientShortArray(short length, byte event)(Code) | | |
jvmResumeTransaction | native public static void jvmResumeTransaction()(Code) | | |
jvmSetShort | native public static short jvmSetShort(byte[] bArray, short bOff, short sValue)(Code) | | |
jvmSuspendTransaction | native public static void jvmSuspendTransaction()(Code) | | |
|
|