01: package javacard.framework;
02:
03: public class SystemException extends CardRuntimeException {
04:
05: /*@ static invariant \is_initialized(SystemException); @*/
06: /*@ static invariant _systemInstance != null; @*/
07: private/*@ spec_public @*/static SystemException _systemInstance;
08:
09: public static final short ILLEGAL_VALUE = (short) 1;
10: public static final short NO_TRANSIENT_SPACE = (short) 2;
11: public static final short ILLEGAL_TRANSIENT = (short) 3;
12: public static final short ILLEGAL_AID = (short) 4;
13: public static final short NO_RESOURCE = (short) 5;
14: public static final short ILLEGAL_USE = (short) 6;
15:
16: /*@ exceptional_behavior
17: requires true;
18: signals (SystemException se) se == _systemInstance && se._reason[0] == reason ;
19: assignable _systemInstance._reason[0] ;
20: @*/
21: public static void throwIt(short reason) throws SystemException {
22: _systemInstance.setReason(reason);
23: throw _systemInstance;
24: }
25: }
|