01: package javacard.framework;
02:
03: public class CardRuntimeException extends java.lang.RuntimeException {
04:
05: /*@ static invariant \is_initialized(CardRuntimeException) ; @*/
06: /*@ static invariant _systemInstance != null; @*/
07: private static CardRuntimeException _systemInstance;
08:
09: /*@ invariant _reason != null && _reason.length == 1; @*/
10: /*@ invariant JCSystem.isTransient(_reason) == JCSystem.CLEAR_ON_RESET ; @*/
11: protected/*@ spec_public @*/short[] _reason;
12:
13: /*@ normal_behavior
14: requires true;
15: ensures \old(_systemInstance) == null ==> _systemInstance == this;
16: assignable _reason, _reason[0], _systemInstance;
17: @*/
18: public CardRuntimeException() {
19: _reason = JCSystem.makeTransientShortArray((short) 1,
20: JCSystem.CLEAR_ON_RESET);
21: if (_systemInstance == null)
22: _systemInstance = this ;
23: }
24:
25: /*@ normal_behavior
26: requires true;
27: ensures _reason[0] == reason;
28: ensures \old(_systemInstance) == null ==> _systemInstance == this;
29: assignable _reason, _reason[0], _systemInstance;
30: @*/
31: public CardRuntimeException(short reason) {
32: _reason = JCSystem.makeTransientShortArray((short) 1,
33: JCSystem.CLEAR_ON_RESET);
34: _reason[0] = reason;
35: if (_systemInstance == null)
36: _systemInstance = this ;
37: }
38:
39: /*@ normal_behavior
40: requires true;
41: ensures \result == _reason[0];
42: assignable \nothing;
43: @*/
44: public short getReason() {
45: return _reason[0];
46: }
47:
48: /*@ normal_behavior
49: requires true;
50: ensures _reason[0] == reason ;
51: assignable _reason[0] ;
52: @*/
53: public void setReason(short reason) {
54: _reason[0] = reason;
55: }
56:
57: /*@ exceptional_behavior
58: requires true;
59: signals (CardRuntimeException cre) cre == _systemInstance && cre._reason[0] == reason ;
60: assignable _systemInstance._reason[0] ;
61: @*/
62: public static void throwIt(short reason)
63: throws CardRuntimeException {
64: _systemInstance.setReason(reason);
65: throw _systemInstance;
66: }
67:
68: }
|