getJavaCardTransient {
\schemaVar \program MethodName [ name = nativeKeYGetTransient ] #getTransient ;
\find ( ==> \modality{#allmodal}{..
#lhs = #jcsystemType.#getTransient(#se)@#jcsystemType;
...}\endmodality post )
"Normal Execution" [ main ] : \replacewith ( ==> { #lhs := select <[ int ]> ( heap , #se , java.lang.Object #$transient ) } \modality{#allmodal}{.. ...}\endmodality post ) ;
"#se is not null" : \replacewith ( ==> #se != null )
\heuristics (simplify_prog )
};defined in: javaRules.key Line: 98 Offset :4setJavaCardTransient {
\schemaVar \program MethodName [ name = nativeKeYSetTransient ] #setTransient ;
\find ( ==> \modality{#allmodal}{..
#jcsystemType.#setTransient(#se, #se1)@#jcsystemType;
...}\endmodality post )
"Normal Execution" [ main ] : \replacewith ( ==> { heap := store ( heap , #se , java.lang.Object #$transient , #se1 ) } \modality{#allmodal}{.. ...}\endmodality post ) ;
"#se is not null" : \replacewith ( ==> #se != null )
\heuristics (simplify_prog )
};defined in: javaRules.key Line: 113 Offset :4beginJavaCardTransactionAPI {
\find ( ==> \modality{#allmodal}{..
#jcsystemType.#beginTransaction()@#jcsystemType;
...}\endmodality post )
\replacewith ( ==> \modality{#allmodal}{.. #beginJavaCardTransaction; ...}\endmodality post )
\heuristics (simplify_prog )
};defined in: javaRules.key Line: 128 Offset :4commitJavaCardTransactionAPI {
\find ( ==> \modality{#allmodal}{..
#jcsystemType.#commitTransaction()@#jcsystemType;
...}\endmodality post )
\replacewith ( ==> \modality{#allmodal}{.. #commitJavaCardTransaction; ...}\endmodality post )
\heuristics (simplify_prog )
};defined in: javaRules.key Line: 138 Offset :4abortJavaCardTransactionAPI {
\find ( ==> \modality{#allmodal}{..
#jcsystemType.#abortTransaction()@#jcsystemType;
...}\endmodality post )
\replacewith ( ==> \modality{#allmodal}{.. #abortJavaCardTransaction; ...}\endmodality post )
\heuristics (simplify_prog )
};defined in: javaRules.key Line: 148 Offset :4beginJavaCardTransactionDiamond {
\find ( ==> \<{..
#beginJavaCardTransaction;
...}\> post )
\replacewith ( ==> { savedHeap := heap } \diamond_transaction{.. ...}\endmodality post )
\heuristics (simplify_prog )
\displayname "beginJavaCardTransaction"
};defined in: javaRules.key Line: 158 Offset :4beginJavaCardTransactionBox {
\find ( ==> \[{..
#beginJavaCardTransaction;
...}\] post )
\replacewith ( ==> { savedHeap := heap } \box_transaction{.. ...}\endmodality post )
\heuristics (simplify_prog )
\displayname "beginJavaCardTransaction"
};defined in: javaRules.key Line: 169 Offset :4commitJavaCardTransactionDiamond {
\find ( ==> \diamond_transaction{..
#commitJavaCardTransaction;
...}\endmodality post )
\replacewith ( ==> \<{.. ...}\> post )
\heuristics (simplify_prog )
\displayname "commitJavaCardTransaction"
};defined in: javaRules.key Line: 180 Offset :4commitJavaCardTransactionBox {
\find ( ==> \box_transaction{..
#commitJavaCardTransaction;
...}\endmodality post )
\replacewith ( ==> \[{.. ...}\] post )
\heuristics (simplify_prog )
\displayname "commitJavaCardTransaction"
};defined in: javaRules.key Line: 191 Offset :4finishJavaCardTransactionDiamond {
\find ( ==> \diamond_transaction{..
#finishJavaCardTransaction;
...}\endmodality post )
\replacewith ( ==> \<{.. ...}\> post )
\heuristics (simplify_prog )
\displayname "finishJavaCardTransaction"
};defined in: javaRules.key Line: 202 Offset :4finishJavaCardTransactionBox {
\find ( ==> \box_transaction{..
#finishJavaCardTransaction;
...}\endmodality post )
\replacewith ( ==> \[{.. ...}\] post )
\heuristics (simplify_prog )
\displayname "finishJavaCardTransaction"
};defined in: javaRules.key Line: 213 Offset :4abortJavaCardTransactionDiamond {
\find ( ==> \diamond_transaction{..
#abortJavaCardTransaction;
...}\endmodality post )
\replacewith ( ==> { heap := anon ( savedHeap , allObjects ( java.lang.Object #$transactionConditionallyUpdated ) , heap ) } \<{.. ...}\> post )
\heuristics (simplify_prog )
\displayname "abortJavaCardTransaction"
};defined in: javaRules.key Line: 224 Offset :4abortJavaCardTransactionBox {
\find ( ==> \box_transaction{..
#abortJavaCardTransaction;
...}\endmodality post )
\replacewith ( ==> { heap := anon ( savedHeap , allObjects ( java.lang.Object #$transactionConditionallyUpdated ) , heap ) } \[{.. ...}\] post )
\heuristics (simplify_prog )
\displayname "abortJavaCardTransaction"
};defined in: javaRules.key Line: 235 Offset :4emptyModality {
\schemaVar \modalOperator { diamond , box } #normal ;
\find ( \modality{#normal}{}\endmodality ( post ) )
\replacewith ( post )
\heuristics (simplify_prog )
};defined in: javaRules.key Line: 250 Offset :4