001: package javacard.framework;
002:
003: import de.uka.ilkd.key.javacard.*;
004:
005: /** Some of the methods in this class do not have any spec. This
006: * is because it is better to execute them symbolically (inline the
007: * implementation) in a KeY proof and let dedicated taclets for jvm*
008: * methods take care of the rest. Such no spec methods are marked
009: * with "no spec"
010: */
011: public final class JCSystem {
012:
013: public static final byte NOT_A_TRANSIENT_OBJECT = (byte) 0;
014: public static final byte CLEAR_ON_RESET = (byte) 1;
015: public static final byte CLEAR_ON_DESELECT = (byte) 2;
016:
017: public static final byte MEMORY_TYPE_PERSISTENT = (byte) 0;
018: public static final byte MEMORY_TYPE_TRANSIENT_RESET = (byte) 1;
019: public static final byte MEMORY_TYPE_TRANSIENT_DESELECT = (byte) 2;
020:
021: private static final short API_VERSION = (short) 0x0202;
022:
023: /*@ static invariant _transactionDepth >= 0; @*/
024: private/*@ spec_public @*/static byte _transactionDepth;
025:
026: // no spec
027: public static byte isTransient(Object theObj) {
028: if (theObj == null)
029: return NOT_A_TRANSIENT_OBJECT;
030: return KeYJCSystem.jvmIsTransient(theObj);
031: }
032:
033: // no spec
034: public static boolean[] makeTransientBooleanArray(short length,
035: byte event) throws SystemException {
036: if (event != CLEAR_ON_RESET && event != CLEAR_ON_DESELECT)
037: SystemException.throwIt(SystemException.ILLEGAL_VALUE);
038: return KeYJCSystem.jvmMakeTransientBooleanArray(length, event);
039: }
040:
041: // no spec
042: public static byte[] makeTransientByteArray(short length, byte event)
043: throws SystemException {
044: if (event != CLEAR_ON_RESET && event != CLEAR_ON_DESELECT)
045: SystemException.throwIt(SystemException.ILLEGAL_VALUE);
046: return KeYJCSystem.jvmMakeTransientByteArray(length, event);
047: }
048:
049: // no spec
050: public static short[] makeTransientShortArray(short length,
051: byte event) throws SystemException {
052: if (event != CLEAR_ON_RESET && event != CLEAR_ON_DESELECT)
053: SystemException.throwIt(SystemException.ILLEGAL_VALUE);
054: return KeYJCSystem.jvmMakeTransientShortArray(length, event);
055: }
056:
057: // no spec
058: public static Object[] makeTransientObjectArray(short length,
059: byte event) throws SystemException {
060: if (event != CLEAR_ON_RESET && event != CLEAR_ON_DESELECT)
061: SystemException.throwIt(SystemException.ILLEGAL_VALUE);
062: return KeYJCSystem.jvmMakeTransientObjectArray(length, event);
063: }
064:
065: /*@ normal_behavior
066: requires true;
067: ensures \result == API_VERSION;
068: assignable \nothing;
069: @*/
070: public static short getVersion() {
071: return API_VERSION;
072: }
073:
074: // no spec
075: public static void beginTransaction() throws TransactionException {
076: if (_transactionDepth != 0)
077: TransactionException
078: .throwIt(TransactionException.IN_PROGRESS);
079: _transactionDepth++;
080: KeYJCSystem.jvmBeginTransaction();
081: }
082:
083: // no spec
084: public static void abortTransaction() throws TransactionException {
085: if (_transactionDepth == 0)
086: TransactionException
087: .throwIt(TransactionException.NOT_IN_PROGRESS);
088: KeYJCSystem.jvmAbortTransaction();
089: _transactionDepth--;
090: }
091:
092: // no spec
093: public static void commitTransaction() throws TransactionException {
094: if (_transactionDepth == 0)
095: TransactionException
096: .throwIt(TransactionException.NOT_IN_PROGRESS);
097: KeYJCSystem.jvmCommitTransaction();
098: _transactionDepth--;
099: }
100:
101: /*@ normal_behavior
102: requires true;
103: ensures \result == _transactionDepth;
104: assignable \nothing;
105: @*/
106: public static byte getTransactionDepth() {
107: return _transactionDepth;
108: }
109:
110: }
|