javaRules.key

Requires: \includeassertions;

requires assertions

Taclets

Enabled under choices: programRules:Java JavaCard:on

getJavaCardTransient

getJavaCardTransient  {
\schemaVar   \program  MethodName [ name =   nativeKeYGetTransient ]  #getTransient;
\find ( ==>           \modality{#allmodal}{..
                   #lhs = #jcsystemType.#getTransient(#se)@#jcsystemType;
                ...}\endmodality             post )
  "Normal Execution" :  \replacewith ( ==>                 {                  #lhs:=                int ::  select   (                   heap ,                    #se,                   java.lang.Object ::   )} \modality{#allmodal}{.. ...}\endmodality             post );
  "#se is not null" :  \replacewith ( ==>                     #se!=           null )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 98 Offset :4

setJavaCardTransient

setJavaCardTransient  {
\schemaVar   \program  MethodName [ name =   nativeKeYSetTransient ]  #setTransient;
\find ( ==>           \modality{#allmodal}{..
                   #jcsystemType.#setTransient(#se, #se1)@#jcsystemType;
                ...}\endmodality             post )
  "Normal Execution" :  \replacewith ( ==>                 {                  heap :=                 store   (                   heap ,                    #se,                   java.lang.Object ::   ,                    #se1)} \modality{#allmodal}{.. ...}\endmodality             post );
  "#se is not null" :  \replacewith ( ==>                     #se!=           null )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 113 Offset :4

beginJavaCardTransactionAPI

beginJavaCardTransactionAPI  {
\find ( ==>           \modality{#allmodal}{..
                   #jcsystemType.#beginTransaction()@#jcsystemType;
                ...}\endmodality             post )
  \replacewith ( ==>           \modality{#allmodal}{.. #beginJavaCardTransaction; ...}\endmodality             post )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 128 Offset :4

commitJavaCardTransactionAPI

commitJavaCardTransactionAPI  {
\find ( ==>           \modality{#allmodal}{..
                   #jcsystemType.#commitTransaction()@#jcsystemType;
                ...}\endmodality             post )
  \replacewith ( ==>           \modality{#allmodal}{.. #commitJavaCardTransaction; ...}\endmodality             post )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 138 Offset :4

abortJavaCardTransactionAPI

abortJavaCardTransactionAPI  {
\find ( ==>           \modality{#allmodal}{..
                   #jcsystemType.#abortTransaction()@#jcsystemType;
                ...}\endmodality             post )
  \replacewith ( ==>           \modality{#allmodal}{.. #abortJavaCardTransaction; ...}\endmodality             post )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 148 Offset :4

beginJavaCardTransactionDiamond

beginJavaCardTransactionDiamond  {
\find ( ==>           \<{..
                   #beginJavaCardTransaction;
                ...}\>             post )
  \replacewith ( ==>                 {                  savedHeap :=                 heap } \diamond_transaction{.. ...}\endmodality             post )
\heuristics  (simplify_prog )
\displayname   "beginJavaCardTransaction" 

};

defined in: javaRules.key Line: 158 Offset :4

beginJavaCardTransactionBox

beginJavaCardTransactionBox  {
\find ( ==>           \[{..
                   #beginJavaCardTransaction;
                ...}\]             post )
  \replacewith ( ==>                 {                  savedHeap :=                 heap } \box_transaction{.. ...}\endmodality             post )
\heuristics  (simplify_prog )
\displayname   "beginJavaCardTransaction" 

};

defined in: javaRules.key Line: 169 Offset :4

commitJavaCardTransactionDiamond

commitJavaCardTransactionDiamond  {
\find ( ==>           \diamond_transaction{..
                   #commitJavaCardTransaction;
                ...}\endmodality             post )
  \replacewith ( ==>           \<{.. ...}\>             post )
\heuristics  (simplify_prog )
\displayname   "commitJavaCardTransaction" 

};

defined in: javaRules.key Line: 180 Offset :4

commitJavaCardTransactionBox

commitJavaCardTransactionBox  {
\find ( ==>           \box_transaction{..
                   #commitJavaCardTransaction;
                ...}\endmodality             post )
  \replacewith ( ==>           \[{.. ...}\]             post )
\heuristics  (simplify_prog )
\displayname   "commitJavaCardTransaction" 

};

defined in: javaRules.key Line: 191 Offset :4

finishJavaCardTransactionDiamond

finishJavaCardTransactionDiamond  {
\find ( ==>           \diamond_transaction{..
                   #finishJavaCardTransaction;
                ...}\endmodality             post )
  \replacewith ( ==>           \<{.. ...}\>             post )
\heuristics  (simplify_prog )
\displayname   "finishJavaCardTransaction" 

};

defined in: javaRules.key Line: 202 Offset :4

finishJavaCardTransactionBox

finishJavaCardTransactionBox  {
\find ( ==>           \box_transaction{..
                   #finishJavaCardTransaction;
                ...}\endmodality             post )
  \replacewith ( ==>           \[{.. ...}\]             post )
\heuristics  (simplify_prog )
\displayname   "finishJavaCardTransaction" 

};

defined in: javaRules.key Line: 213 Offset :4

abortJavaCardTransactionDiamond

abortJavaCardTransactionDiamond  {
\find ( ==>           \diamond_transaction{..
                   #abortJavaCardTransaction;
                ...}\endmodality             post )
  \replacewith ( ==>                 {                  heap :=                 anon   (                   savedHeap ,                    allObjects   (                  java.lang.Object ::   ),                    heap )} \<{.. ...}\>             post )
\heuristics  (simplify_prog )
\displayname   "abortJavaCardTransaction" 

};

defined in: javaRules.key Line: 224 Offset :4

abortJavaCardTransactionBox

abortJavaCardTransactionBox  {
\find ( ==>           \box_transaction{..
                   #abortJavaCardTransaction;
                ...}\endmodality             post )
  \replacewith ( ==>                 {                  heap :=                 anon   (                   savedHeap ,                    allObjects   (                  java.lang.Object ::   ),                    heap )} \[{.. ...}\]             post )
\heuristics  (simplify_prog )
\displayname   "abortJavaCardTransaction" 

};

defined in: javaRules.key Line: 235 Offset :4

Taclets

Enabled under choices: programRules:Java

emptyModality

emptyModality  {
\schemaVar   \modalOperator  {  diamond ,  box } #normal;
\find (          \modality{#normal}{}\endmodality            (                   post ))
  \replacewith (                    post )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 250 Offset :4

emptyModalityBoxTransaction

emptyModalityBoxTransaction  {
\find (          \box_transaction{  }\endmodality            (                   post ))
  "Unbalanced Transaction" :  \replacewith (                    true )
\heuristics  (simplify_prog )
\displayname   "emptyModality" 

};

defined in: javaRules.key Line: 257 Offset :4

emptyModalityDiamondTransaction

emptyModalityDiamondTransaction  {
\find (          \diamond_transaction{  }\endmodality            (                   post ))
  "Unbalanced Transaction" :  \replacewith (                    false )
\heuristics  (simplify_prog )
\displayname   "emptyModality" 

};

defined in: javaRules.key Line: 265 Offset :4

returnUnfold

returnUnfold  {
\find (          \modality{#allmodal}{.. return #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v0=#nse; return #v0; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "returnUnfold" 

};

defined in: javaRules.key Line: 273 Offset :4

deleteMergePoint

deleteMergePoint  {
\find (          \modality{#allmodal}{.. merge_point(#lhs); ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , merge_point )

};

defined in: javaRules.key Line: 281 Offset :4

assignment

assignment  {
\find (          \modality{#allmodal}{.. #loc = #se; ...}\endmodality            (                   post ))
  \replacewith (                {                  #loc:=                 #se} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 291 Offset :4

Taclets

Enabled under choices: programRules:Java permissions:off

assignment_write_array_this_access_normalassign

assignment_write_array_this_access_normalassign  {
\find (          \modality{#allmodal}{.#pm@#t(#v).. this[#se]=#se0; ...}\endmodality            (                   post ))
  \replacewith (                   (                   lt   (                   #se,                    length   (                   #v))&             lt   (               -       1 ,                    #se))->            {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment" 

};

defined in: javaRules.key Line: 301 Offset :4

Taclets

Enabled under choices: programRules:Java permissions:on

assignment_write_array_this_access_normalassign

assignment_write_array_this_access_normalassign  {
\find (          \modality{#allmodal}{.#pm@#t(#v).. this[#se]=#se0; ...}\endmodality            (                   post ))
  \replacewith (                   (                   lt   (                   #se,                    length   (                   #v))&             lt   (               -       1 ,                    #se)&             writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    arr   (                   #se))))->            {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment" 

};

defined in: javaRules.key Line: 311 Offset :4

Taclets

Enabled under choices: programRules:Java

eval_array_this_access

eval_array_this_access  {
\find (          \modality{#allmodal}{.. this[#nse]=#se0; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v0=#nse; this[#v0]=#se0; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "eval_array_access" 

};

defined in: javaRules.key Line: 323 Offset :4

array_self_reference

array_self_reference  {
\schemaVar   \term Heap   heapSV ;
\assumes (                     wellFormed   (                   heapSV )==>                     array =           null )
\find (                    arrayStoreValid   (                   array ,                   G ::  select   (                   heapSV ,                    array ,                    arr   (                   idx ))))
\sameUpdateLevel 
  \replacewith (                    true )
\heuristics  (simplify )

};

defined in: javaRules.key Line: 334 Offset :4

array_self_reference_eq

array_self_reference_eq  {
\schemaVar   \term Heap   heapSV ;
\schemaVar   \term G   EQ ;
\assumes (                     wellFormed   (                   heapSV ),                    G ::  select   (                   heapSV ,                    array ,                    arr   (                   idx ))=           EQ ==>                     array =           null )
\find (                    arrayStoreValid   (                   array ,                    EQ ))
\sameUpdateLevel 
  \replacewith (                    true )
\heuristics  (simplify )

};

defined in: javaRules.key Line: 344 Offset :4

null_can_always_be_stored_in_a_reference_type_array

null_can_always_be_stored_in_a_reference_type_array  {
\assumes (  ==>                     array =           null )
\find (                    arrayStoreValid   (                   array ,                    null ))
\sameUpdateLevel 
\varcond   \replacewith (                    true )
\heuristics  (simplify )

};

defined in: javaRules.key Line: 354 Offset :4

array_store_known_dynamic_array_type

array_store_known_dynamic_array_type  {
\assumes (                    J ::  exactInstance   (                   array )=           TRUE ==>  )
\find (                    arrayStoreValid   (                   array ,                    obj ))
\sameUpdateLevel 
\varcond   \replacewith (                    obj =           null |              #arrayBaseInstanceOf  (                  J ::  exactInstance   (                   array ),                    obj )=           TRUE )
\heuristics  (simplify )
\displayname   "known dynamic array type" 

};

defined in: javaRules.key Line: 372 Offset :4

variableDeclaration

variableDeclaration  {
\find (          \modality{#allmodal}{.. #t #v0; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post )) \addprogvars (  #v0)
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "variableDeclaration" 

};

defined in: javaRules.key Line: 397 Offset :4

variableDeclarationFinal

variableDeclarationFinal  {
\find (          \modality{#allmodal}{.. final #t #v0; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post )) \addprogvars (  #v0)
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "variableDeclaration" 

};

defined in: javaRules.key Line: 405 Offset :4

variableDeclarationGhost

variableDeclarationGhost  {
\find (          \modality{#allmodal}{.. ghost #t #v0; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post )) \addprogvars (  #v0)
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "ghostDeclaration" 

};

defined in: javaRules.key Line: 413 Offset :4

variableDeclarationAssign

variableDeclarationAssign  {
\find (          \modality{#allmodal}{.. #t #v0 = #vi; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #t #v0; #v0 = #vi; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "variableDeclaration" 

};

defined in: javaRules.key Line: 421 Offset :4

variableDeclarationFinalAssign

variableDeclarationFinalAssign  {
\find (          \modality{#allmodal}{.. final #t #v0 = #vi; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. final #t #v0; #v0 = #vi; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "variableDeclaration" 

};

defined in: javaRules.key Line: 428 Offset :4

variableDeclarationGhostAssign

variableDeclarationGhostAssign  {
\find (          \modality{#allmodal}{.. ghost #t #v0 = #vi; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. ghost #t #v0; #v0 = #vi; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "ghostDeclaration" 

};

defined in: javaRules.key Line: 435 Offset :4

variableDeclarationMult

variableDeclarationMult  {
\find (          \modality{#allmodal}{.. #multvardecl ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #resolve-multiple-var-decl(#multvardecl); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "variableDeclaration" 

};

defined in: javaRules.key Line: 442 Offset :4

array_post_declaration

array_post_declaration  {
\find (          \modality{#allmodal}{.. #arraypost ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..
                #array-post-declaration(#arraypost);
                              ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 449 Offset :4

throwNull

throwNull  {
\find (          \modality{#allmodal}{.. throw null; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. throw new java.lang.NullPointerException(); ...}\endmodality            (                   post ))
\displayname   "throwNull" 

};

defined in: javaRules.key Line: 460 Offset :4

throwUnfold

throwUnfold  {
\find (          \modality{#allmodal}{.. throw #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v0 = #nse; throw #v0; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "throwUnfold" 

};

defined in: javaRules.key Line: 466 Offset :4

throwLabel

throwLabel  {
\find (          \modality{#allmodal}{.. #lb: throw #se; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. throw #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 476 Offset :4

throwLabelBlock

throwLabelBlock  {
\find (          \modality{#allmodal}{.. #lb: { throw #se; #slist } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. throw #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 482 Offset :4

throwBox

throwBox  {
\find (          \modality{#box}{ throw #se; #slist }\endmodality            (                   post ))
  \replacewith (                    true )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 488 Offset :4

throwDiamond

throwDiamond  {
\find (          \modality{#diamond}{ throw #se; #slist }\endmodality            (                   post ))
  \replacewith (                    false )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 494 Offset :4

tryCatchThrow

tryCatchThrow  {
\find (          \modality{#allmodal}{.. try { throw #se; #slist }
                catch ( #t #v0 ) { #slist1 } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. if ( #se == null ) {
                      try { throw new java.lang.NullPointerException (); }
                      catch ( #t #v0 ) { #slist1 }
                } else if ( #se instanceof #t ) {
                      #t #v0;
                      #v0 = (#t) #se;
                      #slist1
                } else {
                      throw #se;
                } ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryCatchThrow" 

};

defined in: javaRules.key Line: 500 Offset :4

tryMultipleCatchThrow

tryMultipleCatchThrow  {
\find (          \modality{#allmodal}{.. try { throw #se; #slist }
                catch ( #t #v0 ) { #slist1 }
                catch ( #t2 #v1 ) { #slist3 }
                catch #cs ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. if ( #se == null ) {
                     try { throw new java.lang.NullPointerException (); }
                     catch ( #t #v0 ) { #slist1 }
                     catch ( #t2 #v1 ) { #slist3 }
                     catch #cs
                } else if ( #se instanceof #t ) {
                     #t #v0;
                     #v0 = (#t) #se;
                     #slist1
                } else {
                     try { throw #se; }
                     catch ( #t2 #v1 ) { #slist3 }
                     catch #cs
                } ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryCatchThrow" 

};

defined in: javaRules.key Line: 517 Offset :4

tryCatchFinallyThrow

tryCatchFinallyThrow  {
\find (          \modality{#allmodal}{.. try { throw #se; #slist}
                catch ( #t #v0 ) { #slist1 }
                catch #cs
                finally { #slist2 } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. if ( #se == null ) {
                     try { throw new java.lang.NullPointerException (); }
                     catch ( #t #v0 ) { #slist1 }
                     catch #cs
                     finally { #slist2 }
                } else if ( #se instanceof #t ) {
                     try {
                        #t #v0;
                        #v0 = (#t) #se;
                        #slist1
                     } finally { #slist2 }
                } else {
                     try { throw #se; }
                     catch #cs
                     finally { #slist2 }
                } ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryCatchFinallyThrow" 

};

defined in: javaRules.key Line: 540 Offset :4

tryFinallyThrow

tryFinallyThrow  {
\find (          \modality{#allmodal}{.. try { throw #se; #slist }
                finally { #slist2 } ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. if ( #se == null ) {
                     { #slist2 }
                     throw new java.lang.NullPointerException ();
                } else {
                     #typeof(#se) #v0 = #se;
                     { #slist2 }
                     throw #v0;
                } ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryFinallyThrow" 

};

defined in: javaRules.key Line: 568 Offset :4

tryEmpty

tryEmpty  {
\find (          \modality{#allmodal}{.. try {} #cs ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 584 Offset :4

tryFinallyEmpty

tryFinallyEmpty  {
\find (          \modality{#allmodal}{.. try {}
                catch #cs
                finally { #slist2 } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #slist2 }  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryEmpty" 

};

defined in: javaRules.key Line: 590 Offset :4

tryBreakLabel

tryBreakLabel  {
\find (          \modality{#allmodal}{.. try { break #lb; #slist }
                catch #cs ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. break #lb; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryBreak" 

};

defined in: javaRules.key Line: 599 Offset :4

tryFinallyBreakLabel

tryFinallyBreakLabel  {
\find (          \modality{#allmodal}{.. try { break #lb; #slist }
                catch #cs
                finally { #slist2 } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #slist2 } break #lb; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryBreak" 

};

defined in: javaRules.key Line: 607 Offset :4

tryBreak

tryBreak  {
\find (          \modality{#allmodal}{.. try { break; #slist }
                catch #cs ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. break; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryBreak" 

};

defined in: javaRules.key Line: 616 Offset :4

tryFinallyBreak

tryFinallyBreak  {
\find (          \modality{#allmodal}{.. try { break; #slist }
                catch #cs
                finally { #slist2 } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #slist2 } break; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryBreak" 

};

defined in: javaRules.key Line: 624 Offset :4

try_continue_1

try_continue_1  {
\find (          \modality{#allmodal}{.. try { continue #lb; #slist }
                catch #cs ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. continue #lb; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "try_continue" 

};

defined in: javaRules.key Line: 633 Offset :4

try_finally_continue_1

try_finally_continue_1  {
\find (          \modality{#allmodal}{.. try { continue #lb; #slist }
                catch #cs
                finally { #slist2 } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #slist2 } continue #lb; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "try_continue" 

};

defined in: javaRules.key Line: 641 Offset :4

try_continue_2

try_continue_2  {
\find (          \modality{#allmodal}{.. try { continue; #slist }
                catch #cs ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. continue; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "try_continue" 

};

defined in: javaRules.key Line: 650 Offset :4

try_finally_continue_2

try_finally_continue_2  {
\find (          \modality{#allmodal}{.. try { continue; #slist }
                catch #cs
                finally { #slist2 } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #slist2 } continue; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "try_continue" 

};

defined in: javaRules.key Line: 658 Offset :4

tryReturn

tryReturn  {
\find (          \modality{#allmodal}{.. try { return #se; #slist }
                catch #cs ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. return #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryReturn" 

};

defined in: javaRules.key Line: 667 Offset :4

tryFinallyReturn

tryFinallyReturn  {
\find (          \modality{#allmodal}{.. try { return #se; #slist }
                catch #cs
                finally { #slist2 } ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#se) #v0 = #se;
                { #slist2 }
                return #v0; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryReturn" 

};

defined in: javaRules.key Line: 675 Offset :4

tryReturnNoValue

tryReturnNoValue  {
\find (          \modality{#allmodal}{.. try { return; #slist }
                catch #cs ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. return; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryReturn" 

};

defined in: javaRules.key Line: 687 Offset :4

tryFinallyReturnNoValue

tryFinallyReturnNoValue  {
\find (          \modality{#allmodal}{.. try { return; #slist }
                catch #cs
                finally { #slist2 } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #slist2 } return; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "tryReturn" 

};

defined in: javaRules.key Line: 695 Offset :4

preincrement_assignment

preincrement_assignment  {
\find (          \modality{#allmodal}{.. #lhs0 = ++#lhs1; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1+1); #lhs0 = #lhs1;
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 709 Offset :4

preincrement_assignment_attribute

preincrement_assignment_attribute  {
\find (          \modality{#allmodal}{.. #lhs0 = ++#e.#attribute; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #v.#attribute = (#typeof(#attribute))(#v.#attribute+1); #lhs0=#v.#attribute;
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 716 Offset :4

preincrement_assignment_array

preincrement_assignment_array  {
\find (          \modality{#allmodal}{.. #lhs0 = ++#e[#e0]; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#e0) #v0=#e0;
                #v[#v0] = (#typeof(#e[#e0]))(#v[#v0]+1); #lhs0=#v[#v0];
                 ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 724 Offset :4

preincrement

preincrement  {
\find (          \modality{#allmodal}{.. ++#lhs1; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1+1);
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 733 Offset :4

preincrement_attribute

preincrement_attribute  {
\find (          \modality{#allmodal}{.. ++#e.#attribute; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #v.#attribute = (#typeof(#attribute))(#v.#attribute+1);
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 740 Offset :4

preincrement_array

preincrement_array  {
\find (          \modality{#allmodal}{.. ++#e[#e0]; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#e0) #v0=#e0;
                   #v[#v0]=(#typeof(#e[#e0]))(#v[#v0]+1);
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 748 Offset :4

predecrement

predecrement  {
\find (          \modality{#allmodal}{.. --#lhs1; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1-1);
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 757 Offset :4

predecrement_attribute

predecrement_attribute  {
\find (          \modality{#allmodal}{.. --#e.#attribute; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #v.#attribute = (#typeof(#attribute))(#v.#attribute-1);
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 764 Offset :4

predecrement_array

predecrement_array  {
\find (          \modality{#allmodal}{.. --#e[#e0]; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#e0) #v0=#e0;
                #v[#v0]=(#typeof(#e[#e0]))(#v[#v0]-1);
                     ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 772 Offset :4

predecrement_assignment

predecrement_assignment  {
\find (          \modality{#allmodal}{.. #lhs0 = --#lhs1; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1-1); #lhs0 = #lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 781 Offset :4

predecrement_assignment_attribute

predecrement_assignment_attribute  {
\find (          \modality{#allmodal}{.. #lhs = --#e.#attribute; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #v.#attribute = (#typeof(#attribute))(#v.#attribute-1); #lhs = #v.#attribute;
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 788 Offset :4

predecrement_assignment_array

predecrement_assignment_array  {
\find (          \modality{#allmodal}{.. #lhs0 = --#e[#e0]; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#e0) #v0=#e0;
                #v[#v0] = (#typeof(#e[#e0]))(#v[#v0]-1); #lhs0 = #v[#v0];
                 ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 796 Offset :4

postincrement_assignment

postincrement_assignment  {
\find (          \modality{#allmodal}{.. #lhs0 = #lhs1++; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#lhs0) #v = #lhs1; #lhs1 = (#typeof(#lhs1))(#lhs1+1); #lhs0 = #v;
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 805 Offset :4

postincrement_assignment_attribute

postincrement_assignment_attribute  {
\find (          \modality{#allmodal}{.. #lhs0 = #e.#attribute++; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#lhs0) #v1=#v.#attribute; #v.#attribute = (#typeof(#attribute))(#v.#attribute+1); #lhs0 = #v1;
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 813 Offset :4

postincrement_assignment_array

postincrement_assignment_array  {
\find (          \modality{#allmodal}{.. #lhs0 = #e[#e0]++; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#e0) #v0=#e0;
                #typeof(#lhs0) #v1=#v[#v0]; #v[#v0] = (#typeof(#e[#e0]))(#v[#v0]+1); #lhs0=#v1;
                 ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 821 Offset :4

postincrement

postincrement  {
\find (          \modality{#allmodal}{.. #lhs1++; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1+1);
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 830 Offset :4

postincrement_attribute

postincrement_attribute  {
\find (          \modality{#allmodal}{.. #e.#attribute++; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #v.#attribute = (#typeof(#attribute))(#v.#attribute+1);
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 837 Offset :4

postincrement_array

postincrement_array  {
\find (          \modality{#allmodal}{.. #e[#e0]++; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#e0) #v0=#e0;
                   #v[#v0]=(#typeof(#e[#e0]))(#v[#v0]+1);
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 845 Offset :4

postdecrement

postdecrement  {
\find (          \modality{#allmodal}{.. #lhs1--; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))#lhs1-1;
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 854 Offset :4

postdecrement_attribute

postdecrement_attribute  {
\find (          \modality{#allmodal}{.. #e.#attribute--; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #v.#attribute = (#typeof(#attribute))(#v.#attribute-1);
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 861 Offset :4

postdecrement_array

postdecrement_array  {
\find (          \modality{#allmodal}{.. #e[#e0]--; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#e0) #v0=#e0;
                #v[#v0]=(#typeof(#e[#e0]))(#v[#v0]-1);
                     ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 869 Offset :4

postdecrement_assignment

postdecrement_assignment  {
\find (          \modality{#allmodal}{.. #lhs0 = #lhs1--; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#lhs0) #v = #lhs1; #lhs1 = (#typeof(#lhs1))(#lhs1-1); #lhs0 = #v; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 878 Offset :4

postdecrement_assignment_attribute

postdecrement_assignment_attribute  {
\find (          \modality{#allmodal}{.. #lhs0 = #e.#attribute--; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#lhs0) #v1=#v.#attribute; #v.#attribute = (#typeof(#attribute))(#v.#attribute-1); #lhs0 = #v1;
                ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 886 Offset :4

postdecrement_assignment_array

postdecrement_assignment_array  {
\find (          \modality{#allmodal}{.. #lhs0 = #e[#e0]--; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v=#e; #typeof(#e0) #v0=#e0;
                #typeof(#lhs0) #v1=#v[#v0]; #v[#v0] = (#typeof(#e[#e0]))(#v[#v0]-1); #lhs0 = #v1;
                 ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )

};

defined in: javaRules.key Line: 894 Offset :4

castToBoolean

castToBoolean  {
\find (          \modality{#allmodal}{.. #lhs = (boolean) #exBool; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = #exBool; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 903 Offset :4

compound_reference_cast_expression

compound_reference_cast_expression  {
\find (          \modality{#allmodal}{.. #lhs = (#npit) #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v = #nse;
                #lhs = (#npit) #v;
                     ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "cast" 

};

defined in: javaRules.key Line: 919 Offset :4

compound_reference_cast_expression_primitive

compound_reference_cast_expression_primitive  {
\find (          \modality{#allmodal}{.. #lhs = (#pit) #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v = #nse;
                #lhs = (#pit) #v;
                     ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "cast" 

};

defined in: javaRules.key Line: 929 Offset :4

delete_unnecessary_cast

delete_unnecessary_cast  {
\find (          \modality{#allmodal}{.. #lhs = (#npit) #se; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#se instanceof #npit)" :  \replacewith (                {                  #lhs:=                 #addCast  (                   #se,                    #lhs)} \modality{#allmodal}{.. ...}\endmodality            (                   post )) \add (                     #se=           null |             G ::  instance   (                   #se)=           TRUE ==>  )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 939 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow

reference_type_cast

reference_type_cast  {
\find (          \modality{#allmodal}{.. #lhs = (#npit) #se; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#se instanceof #npit)" :  \replacewith (                {                  #lhs:=                 #addCast  (                   #se,                    #lhs)} \modality{#allmodal}{.. ...}\endmodality            (                   post )) \add (                     #se=           null |             G ::  instance   (                   #se)=           TRUE ==>  );
  "ClassCastException (!(#se instanceof #npit))" :  \replacewith (          \modality{#allmodal}{.. throw new java.lang.ClassCastException();
                    ...}\endmodality            (                   post )) \add (  ==>                     #se=           null |             G ::  instance   (                   #se)=           TRUE )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 953 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban

reference_type_cast

reference_type_cast  {
\find ( ==>           \modality{#allmodal}{.. #lhs = (#npit) #se; ...}\endmodality            (                   post ))
\varcond   "Normal Execution (#se instanceof #npit)" :  \replacewith ( ==>                 {                  #lhs:=                 #addCast  (                   #se,                    #lhs)} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
  "ClassCastException (!(#se instanceof #npit))" :  \replacewith ( ==>                     false ) \add (  ==>                     #se=           null |             G ::  instance   (                   #se)=           TRUE )
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 969 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

reference_type_cast

reference_type_cast  {
\find (          \modality{#allmodal}{.. #lhs = (#npit) #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  #lhs:=                 #addCast  (                   #se,                    #lhs)} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 984 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow

methodCall

methodCall  {
\find (          \modality{#allmodal}{.. #se.#mn(#selist); ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#se != null )" :  \replacewith (          \modality{#allmodal}{.. #method-call(#se.#mn(#selist)); ...}\endmodality            (                   post )) \add (  ==>                     #se=           null );
  "Null Reference (#se = null)" :  \replacewith (          \modality{#allmodal}{.. throw new java.lang.NullPointerException();
                    ...}\endmodality            (                   post )) \add (                     #se=           null ==>  )
\heuristics  (method_expand )

};

defined in: javaRules.key Line: 995 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban

methodCall

methodCall  {
\find ( ==>           \modality{#allmodal}{.. #se.#mn(#selist); ...}\endmodality            (                   post ))
\varcond   "Normal Execution (#se != null )" :  \replacewith ( ==>           \modality{#allmodal}{.. #method-call(#se.#mn(#selist)); ...}\endmodality            (                   post ));
  "Null Reference (#se = null)" :  \replacewith ( ==>                     false ) \add (                     #se=           null ==>  )
\heuristics  (method_expand )

};

defined in: javaRules.key Line: 1012 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

methodCall

methodCall  {
\find (          \modality{#allmodal}{.. #se.#mn(#selist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #method-call(#se.#mn(#selist)); ...}\endmodality            (                   post ))
\heuristics  (method_expand )

};

defined in: javaRules.key Line: 1028 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow

methodCallWithAssignment

methodCallWithAssignment  {
\find (          \modality{#allmodal}{.. #lhs = #se.#mn(#selist); ...}\endmodality            (                  (                   post )))
\sameUpdateLevel 
\varcond   "Normal Execution (#se != null)" :  \replacewith (          \modality{#allmodal}{.. #typeof(#lhs) #v0;
                      #method-call(#v0, #se.#mn(#selist));
                    #lhs = #v0;
                            ...}\endmodality            (                   post )) \add (  ==>                     #se=           null );
  "Null Reference (#se = null)" :  \replacewith (          \modality{#allmodal}{.. throw new java.lang.NullPointerException();
                    ...}\endmodality            (                   post )) \add (                     #se=           null ==>  )
\heuristics  (method_expand )

};

defined in: javaRules.key Line: 1038 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban

methodCallWithAssignment

methodCallWithAssignment  {
\find ( ==>           \modality{#allmodal}{.. #lhs = #se.#mn(#selist); ...}\endmodality            (                  (                   post )))
\varcond   "Normal Execution (#se != null)" :  \replacewith ( ==>           \modality{#allmodal}{.. #typeof(#lhs) #v0;
                      #method-call(#v0, #se.#mn(#selist));
                    #lhs = #v0;
                            ...}\endmodality            (                   post ));
  "Null Reference (#se = null)" :  \replacewith ( ==>                     false ) \add (                     #se=           null ==>  )
\heuristics  (method_expand )

};

defined in: javaRules.key Line: 1057 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

methodCallWithAssignment

methodCallWithAssignment  {
\find (          \modality{#allmodal}{.. #lhs = #se.#mn(#selist); ...}\endmodality            (                  (                   post )))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#lhs) #v0;
                  #method-call(#v0, #se.#mn(#selist));
                #lhs = #v0;
                        ...}\endmodality            (                   post ))
\heuristics  (method_expand )

};

defined in: javaRules.key Line: 1075 Offset :4

Taclets

Enabled under choices: programRules:Java

methodCallUnfoldArguments

methodCallUnfoldArguments  {
\find (          \modality{#allmodal}{.. #nsmr ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #evaluate-arguments(#nsmr); ...}\endmodality            (                   post ))
\heuristics  (simplify_autoname )

};

defined in: javaRules.key Line: 1088 Offset :4

methodCallUnfoldTarget

methodCallUnfoldTarget  {
\find (          \modality{#allmodal}{.. #nse.#mn(#elist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v0;
                #v0 = #nse; #v0.#mn(#elist); ...}\endmodality            (                   post ))
\heuristics  (simplify_autoname )

};

defined in: javaRules.key Line: 1094 Offset :4

Taclets

Enabled under choices: programRules:Java

methodCallSuper

methodCallSuper  {
\find (          \modality{#allmodal}{.#ex.. super.#mn(#elist); ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #method-call(#ex, super.#mn(#elist));
                ...}\endmodality            (                   post ))
\heuristics  (simplify_autoname , method_expand )

};

defined in: javaRules.key Line: 1108 Offset :4

methodCallWithAssignmentSuper

methodCallWithAssignmentSuper  {
\find (          \modality{#allmodal}{.#ex.. #lhs=super.#mn(#elist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#lhs) #v0;
                   #method-call(#ex, #v0, super.#mn(#elist));
                   #lhs = #v0;
                ...}\endmodality            (                   post ))
\heuristics  (simplify_autoname , method_expand )
\displayname   "methodCallSuper" 

};

defined in: javaRules.key Line: 1118 Offset :4

methodCallWithAssignmentUnfoldArguments

methodCallWithAssignmentUnfoldArguments  {
\find (          \modality{#allmodal}{.. #lhs = #nsmr; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #evaluate-arguments(#lhs = #nsmr); ...}\endmodality            (                   post ))
\heuristics  (simplify_autoname )
\displayname   "methodCallUnfoldArguments" 

};

defined in: javaRules.key Line: 1129 Offset :4

methodCallWithAssignmentUnfoldTarget

methodCallWithAssignmentUnfoldTarget  {
\find (          \modality{#allmodal}{.. #lhs = #nse.#mn(#elist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v0;
                #v0 = #nse; #lhs = #v0.#mn(#elist); ...}\endmodality            (                   post ))
\heuristics  (simplify_autoname )
\displayname   "methodCallUnfoldTarget" 

};

defined in: javaRules.key Line: 1136 Offset :4

methodCallEmpty

methodCallEmpty  {
\find (          \modality{#allmodal}{.. method-frame(#ex){} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1145 Offset :4

methodCallEmptyReturn

methodCallEmptyReturn  {
\find (          \modality{#allmodal}{.. method-frame(#ex){return; #slist} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "methodCallReturn" 

};

defined in: javaRules.key Line: 1151 Offset :4

methodCallReturn

methodCallReturn  {
\find (          \modality{#allmodal}{.. method-frame(#v0, #ex){return #se; #slist} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. method-frame(#ex){ #v0 = #se; } ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "methodCallReturn" 

};

defined in: javaRules.key Line: 1158 Offset :4

methodCallReturnIgnoreResult

methodCallReturnIgnoreResult  {
\find (          \modality{#allmodal}{.. method-frame(#ex){return #se; #slist} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "methodCallReturn" 

};

defined in: javaRules.key Line: 1165 Offset :4

methodBodyExpand

methodBodyExpand  {
\find (          \modality{#allmodal}{.. #mb ...}\endmodality            (                   post ))
  \replacewith (                    #introAtPreDefs  (         \modality{#allmodal}{.. #expand-method-body(#mb); ...}\endmodality            (                   post )))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1172 Offset :4

blockReturnNoValue

blockReturnNoValue  {
\find (          \modality{#allmodal}{.. {return; #slist} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. return;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "blockReturn" 

};

defined in: javaRules.key Line: 1178 Offset :4

blockReturn

blockReturn  {
\find (          \modality{#allmodal}{.. {return #se; #slist} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. return #se;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "blockReturn" 

};

defined in: javaRules.key Line: 1185 Offset :4

blockReturnLabel1

blockReturnLabel1  {
\find (          \modality{#allmodal}{.. #lb: return #se; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. return #se;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "blockReturn (remove label)" 

};

defined in: javaRules.key Line: 1192 Offset :4

blockReturnLabel2

blockReturnLabel2  {
\find (          \modality{#allmodal}{.. #lb: { return #se; #slist } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. return #se;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "blockReturn (remove label)" 

};

defined in: javaRules.key Line: 1199 Offset :4

methodCallThrow

methodCallThrow  {
\find (          \modality{#allmodal}{.. method-frame(#ex){throw #se; #slist} ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. throw #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "methodCallThrow" 

};

defined in: javaRules.key Line: 1206 Offset :4

methodCallParamThrow

methodCallParamThrow  {
\find (          \modality{#allmodal}{.. method-frame(#v0, #ex){throw #se; #slist}
                ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. throw #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "methodCallThrow" 

};

defined in: javaRules.key Line: 1214 Offset :4

throwUnfoldMore

throwUnfoldMore  {
\find (          \modality{#allmodal}{.. throw #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#se) #v0 = #se; throw #v0; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "throwUnfold" 

};

defined in: javaRules.key Line: 1224 Offset :4

blockThrow

blockThrow  {
\find (          \modality{#allmodal}{.. {throw #e; #slist} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. throw #e;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "blockThrow" 

};

defined in: javaRules.key Line: 1232 Offset :4

methodCallEmptyNoreturnBox

methodCallEmptyNoreturnBox  {
\find (          \[{.. method-frame(#v0, #ex){} ...}\]            (                   post ))
  \replacewith (          \[{..  ...}\]            (                   post ))
\heuristics  (simplify_prog )
\displayname   "methodCallEmpty" 

};

defined in: javaRules.key Line: 1239 Offset :4

ifUnfold

ifUnfold  {
\find (          \modality{#allmodal}{.. if(#nse) #s0 ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. boolean #boolv; #boolv = #nse; if(#boolv) #s0 ...}\endmodality            (                   post ))
\heuristics  (simplify_autoname )
\displayname   "ifElseUnfold" 

};

defined in: javaRules.key Line: 1248 Offset :4

ifElseUnfold

ifElseUnfold  {
\find (          \modality{#allmodal}{.. if(#nse) #s0 else #s1 ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. boolean #boolv; #boolv = #nse; if(#boolv) #s0 else{#s1}
                ...}\endmodality            (                   post ))
\heuristics  (simplify_autoname )
\displayname   "ifElseUnfold" 

};

defined in: javaRules.key Line: 1256 Offset :4

if

if  {
\find (          \modality{#allmodal}{.. if(#se) #s0  ...}\endmodality            (                   post ))
  \replacewith (                   \if (                   #se=           TRUE )\then (         \modality{#allmodal}{.. #s0 ...}\endmodality            (                   post ))\else (         \modality{#allmodal}{.. ...}\endmodality            (                   post )))
\displayname   "ifElse" 

};

defined in: javaRules.key Line: 1265 Offset :4

ifElse

ifElse  {
\find (          \modality{#allmodal}{.. if(#se) #s0 else #s1 ...}\endmodality            (                   post ))
  \replacewith (                   \if (                   #se=           TRUE )\then (         \modality{#allmodal}{.. #s0 ...}\endmodality            (                   post ))\else (         \modality{#allmodal}{.. #s1 ...}\endmodality            (                   post )))
\displayname   "ifElse" 

};

defined in: javaRules.key Line: 1273 Offset :4

ifElseSplit

ifElseSplit  {
\find ( ==>           \modality{#allmodal}{.. if(#se) #s0 else #s1 ...}\endmodality            (                   post ))
  "if #se true" :  \replacewith ( ==>           \modality{#allmodal}{.. #s0 ...}\endmodality            (                   post )) \add (                     #se=           TRUE ==>  );
  "if #se false" :  \replacewith ( ==>           \modality{#allmodal}{.. #s1 ...}\endmodality            (                   post )) \add (                     #se=           FALSE ==>  )
\heuristics  (split_if )
\displayname   "ifElseSplit" 

};

defined in: javaRules.key Line: 1281 Offset :4

ifSplit

ifSplit  {
\find ( ==>           \modality{#allmodal}{.. if(#se) #s0  ...}\endmodality            (                   post ))
  "if #se true" :  \replacewith ( ==>           \modality{#allmodal}{.. #s0 ...}\endmodality            (                   post )) \add (                     #se=           TRUE ==>  );
  "if #se false" :  \replacewith ( ==>           \modality{#allmodal}{..  ...}\endmodality            (                   post )) \add (                     #se=           FALSE ==>  )
\heuristics  (split_if )
\displayname   "ifElseSplit" 

};

defined in: javaRules.key Line: 1291 Offset :4

ifElseSplitLeft

ifElseSplitLeft  {
\find (          \modality{#allmodal}{.. if(#se) #s0 else #s1 ...}\endmodality            (                   post )==>  )
  \replacewith (          \modality{#allmodal}{.. #s0 ...}\endmodality            (                   post )==>  ) \add (                     #se=           TRUE ==>  );
  \replacewith (          \modality{#allmodal}{.. #s1 ...}\endmodality            (                   post )==>  ) \add (                     #se=           FALSE ==>  )
\heuristics  (split_if )

};

defined in: javaRules.key Line: 1301 Offset :4

ifSplitLeft

ifSplitLeft  {
\find (          \modality{#allmodal}{.. if(#se) #s0  ...}\endmodality            (                   post )==>  )
  \replacewith (          \modality{#allmodal}{.. #s0 ...}\endmodality            (                   post )==>  ) \add (                     #se=           TRUE ==>  );
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post )==>  ) \add (                     #se=           FALSE ==>  )
\heuristics  (split_if )

};

defined in: javaRules.key Line: 1307 Offset :4

ifTrue

ifTrue  {
\assumes (                     #se=           TRUE ==>  )
\find ( ==>           \modality{#allmodal}{.. if (#se) #s0 ...}\endmodality            (                   post ))
  \replacewith ( ==>           \modality{#allmodal}{.. #s0 ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1313 Offset :4

ifElseTrue

ifElseTrue  {
\assumes (                     #se=           TRUE ==>  )
\find ( ==>           \modality{#allmodal}{.. if (#se) #s0 else #s1 ...}\endmodality            (                   post ))
  \replacewith ( ==>           \modality{#allmodal}{.. #s0 ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1320 Offset :4

ifFalse

ifFalse  {
\assumes (                     #se=           FALSE ==>  )
\find ( ==>           \modality{#allmodal}{.. if (#se) #s0 ...}\endmodality            (                   post ))
  \replacewith ( ==>           \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1327 Offset :4

ifElseFalse

ifElseFalse  {
\assumes (                     #se=           FALSE ==>  )
\find ( ==>           \modality{#allmodal}{.. if (#se) #s0 else #s1 ...}\endmodality            (                   post ))
  \replacewith ( ==>           \modality{#allmodal}{.. #s1 ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1334 Offset :4

ifEnterThen

ifEnterThen  {
\find (          \modality{#allmodal}{.. #loc=true; if (#loc) #s0 ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #loc=true; #s0 ...}\endmodality            (                   post ))
\heuristics  (simplify )

};

defined in: javaRules.key Line: 1341 Offset :4

ifSkipThen

ifSkipThen  {
\find (          \modality{#allmodal}{.. #loc=false; if (#loc) #s0 ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #loc=false; ...}\endmodality            (                   post ))
\heuristics  (simplify )

};

defined in: javaRules.key Line: 1347 Offset :4

ifElseSkipElse

ifElseSkipElse  {
\find (          \modality{#allmodal}{.. #loc=true; if (#loc) #s0 else #s1 ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #loc=true; #s0 ...}\endmodality            (                   post ))
\heuristics  (simplify )

};

defined in: javaRules.key Line: 1353 Offset :4

ifElseSkipThen

ifElseSkipThen  {
\find (          \modality{#allmodal}{.. #loc=false; if (#loc) #s0 else #s1 ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #loc=false; #s1 ...}\endmodality            (                   post ))
\heuristics  (simplify )

};

defined in: javaRules.key Line: 1359 Offset :4

ifEnterThenConditionInBlock

ifEnterThenConditionInBlock  {
\find (          \modality{#allmodal}{.. { #loc=true; } if (#loc) #s0 ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #loc=true; } #s0 ...}\endmodality            (                   post ))
\heuristics  (simplify )
\displayname   "ifEnterThen" 

};

defined in: javaRules.key Line: 1365 Offset :4

ifSkipThenConditionInBlock

ifSkipThenConditionInBlock  {
\find (          \modality{#allmodal}{.. { #loc=false; } if (#loc) #s0 ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #loc=false; } ...}\endmodality            (                   post ))
\heuristics  (simplify )
\displayname   "ifSkipThen" 

};

defined in: javaRules.key Line: 1372 Offset :4

ifElseSkipElseConditionInBlock

ifElseSkipElseConditionInBlock  {
\find (          \modality{#allmodal}{.. { #loc=true;} if (#loc) #s0 else #s1 ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #loc=true;} #s0 ...}\endmodality            (                   post ))
\heuristics  (simplify )
\displayname   "ifElseSkipElse" 

};

defined in: javaRules.key Line: 1379 Offset :4

ifElseSkipThenConditionInBlock

ifElseSkipThenConditionInBlock  {
\find (          \modality{#allmodal}{.. { #loc=false; } if (#loc) #s0 else #s1 ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #loc=false; } #s1 ...}\endmodality            (                   post ))
\heuristics  (simplify )
\displayname   "ifElseSkipThen" 

};

defined in: javaRules.key Line: 1386 Offset :4

switch

switch  {
\find (          \modality{#allmodal}{.. #sw ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #switch-to-if(#sw) ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1396 Offset :4

break

break  {
\find (          \modality{#allmodal}{.. #lb0: break #lb1;  ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #do-break(#lb0: break #lb1;); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1405 Offset :4

blockBreakNoLabel

blockBreakNoLabel  {
\find (          \modality{#allmodal}{.. { break #lb1; #slist} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. break #lb1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "blockBreakNoLabel" 

};

defined in: javaRules.key Line: 1411 Offset :4

blockBreakLabel

blockBreakLabel  {
\find (          \modality{#allmodal}{.. #lb0: {break #lb1; #slist } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #do-break(#lb0: break #lb1;); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1418 Offset :4

blockEmptyLabel

blockEmptyLabel  {
\find (          \modality{#allmodal}{.. #lb:{} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. {}  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "blockEmpty" 

};

defined in: javaRules.key Line: 1424 Offset :4

blockEmpty

blockEmpty  {
\find (          \modality{#allmodal}{.. {} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 1431 Offset :4

unusedLabel

unusedLabel  {
\find (          \modality{#allmodal}{.. #lb: #s ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #s ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1437 Offset :4

emptyStatement

emptyStatement  {
\find (          \modality{#allmodal}{.. ; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 1444 Offset :4

synchronizedBlockEvalSync

synchronizedBlockEvalSync  {
\find (          \modality{#allmodal}{.. synchronized(#nsencr){ #slist } ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nsencr) #loc=#nsencr; synchronized(#loc){ #slist } ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 1450 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban

synchronizedBlockEmpty

synchronizedBlockEmpty  {
\find ( ==>           \modality{#allmodal}{.. synchronized(#se){} ...}\endmodality            (                   post ))
\varcond   "Normal Execution" :  \replacewith ( ==>           \modality{#allmodal}{..  ...}\endmodality            (                   post ));
  "#se is not null" :  \replacewith ( ==>                     #se!=           null )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 1461 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

synchronizedBlockEmpty

synchronizedBlockEmpty  {
\find ( ==>           \modality{#allmodal}{.. synchronized(#se){} ...}\endmodality            (                   post ))
\varcond   "Normal Execution" :  \replacewith ( ==>           \modality{#allmodal}{..  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 1475 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow

synchronizedBlockEmpty

synchronizedBlockEmpty  {
\find ( ==>           \modality{#allmodal}{.. synchronized(#se){} ...}\endmodality            (                   post ))
\varcond   \replacewith ( ==>           \modality{#allmodal}
                {.. if(#se==null){throw new java.lang.NullPointerException();}  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 1487 Offset :4

Taclets

Enabled under choices: programRules:Java

synchronizedBlockEmpty2

synchronizedBlockEmpty2  {
\find (          \modality{#allmodal}{.. synchronized(#cr){} ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "synchronizedBlockEmpty" 

};

defined in: javaRules.key Line: 1499 Offset :4

instanceof_eval

instanceof_eval  {
\find (          \modality{#allmodal}{.. #v = #nse instanceof #t; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#nse) #v0=#nse;
                #v=#v0 instanceof #t;...}\endmodality            (                   post ))
\heuristics  (simplify_autoname )

};

defined in: javaRules.key Line: 1510 Offset :4

insert_constant_value

insert_constant_value  {
\find (                    #cv)
  \replacewith (                    #constantvalue  (                   #cv))
\heuristics  (concrete )

};

defined in: javaRules.key Line: 1522 Offset :4

condition

condition  {
\find (          \modality{#allmodal}{.. #lhs = #e0 ? #e1 : #e2; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. if(#e0) {#lhs = #e1;}
                else {#lhs = #e2;} ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , split_if )

};

defined in: javaRules.key Line: 1533 Offset :4

condition_not_simple

condition_not_simple  {
\find (          \modality{#allmodal}{.. #lhs = #nse ? #se1 : #se2; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v0 = #nse; #lhs = #v0 ? #se1 : #se2; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "condition" 

};

defined in: javaRules.key Line: 1540 Offset :4

condition_simple

condition_simple  {
\find (          \modality{#allmodal}{.. #lhs = #se0 ? #se1 : #se2; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   #se0=           TRUE )\then (                   #se1)\else (                   #se2)} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "condition" 

};

defined in: javaRules.key Line: 1548 Offset :4

equality_comparison_new

equality_comparison_new  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 == #senf1; ...}\endmodality            (                   post ))
  \replacewith (                   \if (         !             #senf0=           #senf1)\then (         \modality{#allmodal}{.. #lhs = false; ...}\endmodality            (                   post ))\else (         \modality{#allmodal}{.. #lhs = true;  ...}\endmodality            (                   post )))
\heuristics  (obsolete , simplify_prog , split_if )
\displayname   "equality comparison" 

};

defined in: javaRules.key Line: 1560 Offset :4

equality_comparison_simple

equality_comparison_simple  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 == #senf1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   #senf0=           #senf1)\then (                   TRUE )\else (                   FALSE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "equality comparison" 

};

defined in: javaRules.key Line: 1569 Offset :4

inequality_comparison_new

inequality_comparison_new  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 != #senf1; ...}\endmodality            (                   post ))
  \replacewith (                   \if (         !             #senf0=           #senf1)\then (         \modality{#allmodal}{.. #lhs = true; ...}\endmodality            (                   post ))\else (         \modality{#allmodal}{.. #lhs = false; ...}\endmodality            (                   post )))
\heuristics  (obsolete , simplify_prog , split_if )
\displayname   "inequality comparison" 

};

defined in: javaRules.key Line: 1577 Offset :4

inequality_comparison_simple

inequality_comparison_simple  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 != #senf1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   #senf0=           #senf1)\then (                   FALSE )\else (                   TRUE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "inequality comparison" 

};

defined in: javaRules.key Line: 1585 Offset :4

less_than_comparison_new

less_than_comparison_new  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 < #senf1; ...}\endmodality            (                   post ))
  \replacewith (                   \if (                   lt   (                   #senf0,                    #senf1))\then (         \modality{#allmodal}{.. #lhs = true;  ...}\endmodality            (                   post ))\else (         \modality{#allmodal}{.. #lhs = false; ...}\endmodality            (                   post )))
\heuristics  (obsolete , simplify_prog , split_if )
\displayname   "lesser than distinction" 

};

defined in: javaRules.key Line: 1593 Offset :4

less_than_comparison_simple

less_than_comparison_simple  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 < #senf1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   lt   (                   #senf0,                    #senf1))\then (                   TRUE )\else (                   FALSE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "lesser than distinction" 

};

defined in: javaRules.key Line: 1601 Offset :4

less_equal_than_comparison_new

less_equal_than_comparison_new  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 <= #senf1; ...}\endmodality            (                   post ))
  \replacewith (                   \if (                   leq   (                   #senf0,                    #senf1))\then (         \modality{#allmodal}{.. #lhs = true; ...}\endmodality            (                   post ))\else (         \modality{#allmodal}{.. #lhs = false; ...}\endmodality            (                   post )))
\heuristics  (obsolete , simplify_prog , split_if )
\displayname   "less-or-equal than distinction" 

};

defined in: javaRules.key Line: 1609 Offset :4

less_equal_than_comparison_simple

less_equal_than_comparison_simple  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 <= #senf1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   leq   (                   #senf0,                    #senf1))\then (                   TRUE )\else (                   FALSE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "less-or-equal than distinction" 

};

defined in: javaRules.key Line: 1617 Offset :4

greater_than_comparison_new

greater_than_comparison_new  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 > #senf1; ...}\endmodality            (                   post ))
  \replacewith (                   \if (                   gt   (                   #senf0,                    #senf1))\then (         \modality{#allmodal}{.. #lhs = true;  ...}\endmodality            (                   post ))\else (         \modality{#allmodal}{.. #lhs = false; ...}\endmodality            (                   post )))
\heuristics  (obsolete , simplify_prog , split_if )
\displayname   "greater than distinction" 

};

defined in: javaRules.key Line: 1625 Offset :4

greater_than_comparison_simple

greater_than_comparison_simple  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 > #senf1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   gt   (                   #senf0,                    #senf1))\then (                   TRUE )\else (                   FALSE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "greater than distinction" 

};

defined in: javaRules.key Line: 1633 Offset :4

greater_equal_than_comparison_new

greater_equal_than_comparison_new  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 >= #senf1; ...}\endmodality            (                   post ))
  \replacewith (                   \if (                   geq   (                   #senf0,                    #senf1))\then (         \modality{#allmodal}{.. #lhs = true; ...}\endmodality            (                   post ))\else (         \modality{#allmodal}{.. #lhs = false; ...}\endmodality            (                   post )))
\heuristics  (obsolete , simplify_prog , split_if )
\displayname   "greater-or-equal than distinction" 

};

defined in: javaRules.key Line: 1641 Offset :4

greater_equal_than_comparison_simple

greater_equal_than_comparison_simple  {
\find (          \modality{#allmodal}{.. #lhs = #senf0 >= #senf1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   geq   (                   #senf0,                    #senf1))\then (                   TRUE )\else (                   FALSE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "greater-or-equal than distinction" 

};

defined in: javaRules.key Line: 1649 Offset :4

compound_byte_cast_expression

compound_byte_cast_expression  {
\find (          \modality{#allmodal}{.. #lhs = (byte) #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v = #nse; #lhs = (byte) #v;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "cast" 

};

defined in: javaRules.key Line: 1661 Offset :4

compound_short_cast_expression

compound_short_cast_expression  {
\find (          \modality{#allmodal}{.. #lhs = (short) #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v = #nse; #lhs = (short) #v;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "cast" 

};

defined in: javaRules.key Line: 1669 Offset :4

compound_int_cast_expression

compound_int_cast_expression  {
\find (          \modality{#allmodal}{.. #lhs = (int) #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v = #nse; #lhs = (int) #v;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "cast" 

};

defined in: javaRules.key Line: 1677 Offset :4

compound_long_cast_expression

compound_long_cast_expression  {
\find (          \modality{#allmodal}{.. #lhs = (long) #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v = #nse; #lhs = (long) #v;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "cast" 

};

defined in: javaRules.key Line: 1685 Offset :4

compound_assignment_op_mul_attr

compound_assignment_op_mul_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute *= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute * #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1697 Offset :4

compound_assignment_op_mul_array

compound_assignment_op_mul_array  {
\find (          \modality{#allmodal}{.. #e0[#e] *= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] * #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1704 Offset :4

compound_assignment_op_mul

compound_assignment_op_mul  {
\find (          \modality{#allmodal}{.. #lhs *= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs * (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1712 Offset :4

compound_assignment_op_div_attr

compound_assignment_op_div_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute /= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute / #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1718 Offset :4

compound_assignment_op_div_array

compound_assignment_op_div_array  {
\find (          \modality{#allmodal}{.. #e0[#e] /= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e; #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] / #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1725 Offset :4

compound_assignment_op_div

compound_assignment_op_div  {
\find (          \modality{#allmodal}{.. #lhs /= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs / (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1732 Offset :4

compound_assignment_op_mod_attr

compound_assignment_op_mod_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute %= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute % #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1738 Offset :4

compound_assignment_op_mod_array

compound_assignment_op_mod_array  {
\find (          \modality{#allmodal}{.. #e0[#e] %= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] % #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1745 Offset :4

compound_assignment_op_mod

compound_assignment_op_mod  {
\find (          \modality{#allmodal}{.. #lhs %= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs % (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1753 Offset :4

compound_assignment_op_plus_attr

compound_assignment_op_plus_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute += #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute + #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1759 Offset :4

compound_assignment_op_plus_array

compound_assignment_op_plus_array  {
\find (          \modality{#allmodal}{.. #e0[#e] += #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] + #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1766 Offset :4

compound_assignment_op_plus

compound_assignment_op_plus  {
\find (          \modality{#allmodal}{.. #lhs += #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs + (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1774 Offset :4

compound_assignment_op_minus_attr

compound_assignment_op_minus_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute -= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute - #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1780 Offset :4

compound_assignment_op_minus_array

compound_assignment_op_minus_array  {
\find (          \modality{#allmodal}{.. #e0[#e] -= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] - #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1787 Offset :4

compound_assignment_op_minus

compound_assignment_op_minus  {
\find (          \modality{#allmodal}{.. #lhs -= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs - (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1795 Offset :4

compound_assignment_op_shiftleft_attr

compound_assignment_op_shiftleft_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute <<= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute << #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1801 Offset :4

compound_assignment_op_shiftleft_array

compound_assignment_op_shiftleft_array  {
\find (          \modality{#allmodal}{.. #e0[#e] <<= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] << #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1808 Offset :4

compound_assignment_op_shiftleft

compound_assignment_op_shiftleft  {
\find (          \modality{#allmodal}{.. #lhs <<= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs << (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1816 Offset :4

compound_assignment_op_shiftright_attr

compound_assignment_op_shiftright_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute >>= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute >> #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1822 Offset :4

compound_assignment_op_shiftright_array

compound_assignment_op_shiftright_array  {
\find (          \modality{#allmodal}{.. #e0[#e] >>= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] >> #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1829 Offset :4

compound_assignment_op_shiftright

compound_assignment_op_shiftright  {
\find (          \modality{#allmodal}{.. #lhs >>= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs >> (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1837 Offset :4

compound_assignment_op_unsigned_shiftright_attr

compound_assignment_op_unsigned_shiftright_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute >>>= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute >>> #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1843 Offset :4

compound_assignment_op_unsigned_shiftright_array

compound_assignment_op_unsigned_shiftright_array  {
\find (          \modality{#allmodal}{.. #e0[#e] >>>= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] >>> #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1850 Offset :4

compound_assignment_op_unsigned_shiftright

compound_assignment_op_unsigned_shiftright  {
\find (          \modality{#allmodal}{.. #lhs >>>= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs >>> (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1858 Offset :4

compound_assignment_op_and_attr

compound_assignment_op_and_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute &= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute & #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1864 Offset :4

compound_assignment_op_and_array

compound_assignment_op_and_array  {
\find (          \modality{#allmodal}{.. #e0[#e] &= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] & #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1871 Offset :4

compound_assignment_op_and

compound_assignment_op_and  {
\find (          \modality{#allmodal}{.. #lhs &= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs & (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1879 Offset :4

compound_assignment_op_or_attr

compound_assignment_op_or_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute |= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute | #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1885 Offset :4

compound_assignment_op_or_array

compound_assignment_op_or_array  {
\find (          \modality{#allmodal}{.. #e0[#e] |= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] | #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1892 Offset :4

compound_assignment_op_or

compound_assignment_op_or  {
\find (          \modality{#allmodal}{.. #lhs |= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs | (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1900 Offset :4

compound_assignment_op_xor_attr

compound_assignment_op_xor_attr  {
\find (          \modality{#allmodal}{.. #e0.#attribute ^= #e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v=#e0; #v.#attribute = (#typeof(#attribute))(#v.#attribute ^ #e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1906 Offset :4

compound_assignment_op_xor_array

compound_assignment_op_xor_array  {
\find (          \modality{#allmodal}{.. #e0[#e] ^= #e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0; #typeof(#e) #v1=#e;
                #v0[#v1] = (#typeof(#e0[#e]))(#v0[#v1] ^ #e1); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1913 Offset :4

compound_assignment_op_xor

compound_assignment_op_xor  {
\find (          \modality{#allmodal}{.. #lhs ^= #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = (#typeof(#lhs))(#lhs ^ (#e)); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 1921 Offset :4

eval_order_iterated_assignments_0_0

eval_order_iterated_assignments_0_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]=#e1;
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 1931 Offset :4

eval_order_iterated_assignments_0_1

eval_order_iterated_assignments_0_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute=#e;
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 1943 Offset :4

iterated_assignments_0

iterated_assignments_0  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1=#e; #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 1953 Offset :4

eval_order_iterated_assignments_1_0

eval_order_iterated_assignments_1_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]*=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] * #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 1960 Offset :4

eval_order_iterated_assignments_1_1

eval_order_iterated_assignments_1_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute*=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute * #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 1972 Offset :4

iterated_assignments_1

iterated_assignments_1  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1*=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 * #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 1982 Offset :4

eval_order_iterated_assignments_2_0

eval_order_iterated_assignments_2_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]/=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] / #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 1989 Offset :4

eval_order_iterated_assignments_2_1

eval_order_iterated_assignments_2_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute/=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute / #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2001 Offset :4

iterated_assignments_2

iterated_assignments_2  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1/=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 / #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2011 Offset :4

eval_order_iterated_assignments_3_0

eval_order_iterated_assignments_3_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]%=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] % #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2018 Offset :4

eval_order_iterated_assignments_3_1

eval_order_iterated_assignments_3_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute%=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute % #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2030 Offset :4

iterated_assignments_3

iterated_assignments_3  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1%=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 % #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2040 Offset :4

eval_order_iterated_assignments_4_0

eval_order_iterated_assignments_4_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]+=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] + #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2047 Offset :4

eval_order_iterated_assignments_4_1

eval_order_iterated_assignments_4_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute+=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute + #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2059 Offset :4

iterated_assignments_4

iterated_assignments_4  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1+=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 + #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2069 Offset :4

eval_order_iterated_assignments_5_0

eval_order_iterated_assignments_5_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]-=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] - #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2076 Offset :4

eval_order_iterated_assignments_5_1

eval_order_iterated_assignments_5_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute-=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute - #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2088 Offset :4

iterated_assignments_5

iterated_assignments_5  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1-=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 - #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2098 Offset :4

eval_order_iterated_assignments_6_0

eval_order_iterated_assignments_6_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]<<=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] << #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2105 Offset :4

eval_order_iterated_assignments_6_1

eval_order_iterated_assignments_6_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute<<=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute << #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2117 Offset :4

iterated_assignments_6

iterated_assignments_6  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1<<=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 << #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2127 Offset :4

eval_order_iterated_assignments_7_0

eval_order_iterated_assignments_7_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]>>=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] >> #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2134 Offset :4

eval_order_iterated_assignments_7_1

eval_order_iterated_assignments_7_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute>>=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute >> #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2146 Offset :4

iterated_assignments_7

iterated_assignments_7  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1>>=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 >> #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2156 Offset :4

eval_order_iterated_assignments_8_0

eval_order_iterated_assignments_8_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]>>>=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] >>> #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2163 Offset :4

eval_order_iterated_assignments_8_1

eval_order_iterated_assignments_8_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute>>>=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute >>> #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2175 Offset :4

iterated_assignments_8

iterated_assignments_8  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1>>>=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 >>> #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2185 Offset :4

eval_order_iterated_assignments_9_0

eval_order_iterated_assignments_9_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]&=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] & #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2192 Offset :4

eval_order_iterated_assignments_9_1

eval_order_iterated_assignments_9_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute&=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute & #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2204 Offset :4

iterated_assignments_9

iterated_assignments_9  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1&=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 & #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2214 Offset :4

eval_order_iterated_assignments_10_0

eval_order_iterated_assignments_10_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]|=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] | #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2221 Offset :4

eval_order_iterated_assignments_10_1

eval_order_iterated_assignments_10_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute|=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute | #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2233 Offset :4

iterated_assignments_10

iterated_assignments_10  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1|=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 | #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2243 Offset :4

eval_order_iterated_assignments_11_0

eval_order_iterated_assignments_11_0  {
\find (          \modality{#allmodal}{.. #lhs0=#e0[#e]^=#e1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #typeof(#e) #v1=#e;
                #v0[#v1]= (#typeof(#e0[#e]))(#v0[#v1] ^ #e1);
                #lhs0=#v0[#v1];  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2250 Offset :4

eval_order_iterated_assignments_11_1

eval_order_iterated_assignments_11_1  {
\find (          \modality{#allmodal}{.. #lhs0=#e0.#attribute^=#e; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e0) #v0=#e0;
                #v0.#attribute = (#typeof(#attribute))(#v0.#attribute ^ #e);
                #lhs0=#v0.#attribute;  ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2262 Offset :4

iterated_assignments_11

iterated_assignments_11  {
\find (          \modality{#allmodal}{.. #lhs0=#lhs1^=#e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs1 = (#typeof(#lhs1))(#lhs1 ^ #e); #lhs0=#lhs1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "eval_order_iterated_assignments" 

};

defined in: javaRules.key Line: 2272 Offset :4

elim_double_block

elim_double_block  {
\find (          \modality{#allmodal}{{ #slist }}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{ #slist }\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 2283 Offset :4

elim_double_block_2

elim_double_block_2  {
\find (          \modality{#allmodal}{.. { { #slist } } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #slist } ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "elim_double_block" 

};

defined in: javaRules.key Line: 2289 Offset :4

elim_double_block_3

elim_double_block_3  {
\find (          \modality{#allmodal}{.. { while ( #e ) #s } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. while ( #e ) #s ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "elim_double_block" 

};

defined in: javaRules.key Line: 2296 Offset :4

elim_double_block_4

elim_double_block_4  {
\find (          \modality{#allmodal}{.. { for(#loopInit; #guard; #forupdates) #s } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. for(#loopInit; #guard; #forupdates) #s ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "elim_double_block" 

};

defined in: javaRules.key Line: 2303 Offset :4

elim_double_block_5

elim_double_block_5  {
\find (          \modality{#allmodal}{.. { for(; #guard; #forupdates) #s } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. for(; #guard; #forupdates) #s ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "elim_double_block" 

};

defined in: javaRules.key Line: 2310 Offset :4

elim_double_block_6

elim_double_block_6  {
\find (          \modality{#allmodal}{.. { for(#loopInit; #guard;) #s } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. for(#loopInit; #guard;) #s ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "elim_double_block" 

};

defined in: javaRules.key Line: 2317 Offset :4

elim_double_block_7

elim_double_block_7  {
\find (          \modality{#allmodal}{.. { for(; #guard;) #s } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. for(; #guard;) #s ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "elim_double_block" 

};

defined in: javaRules.key Line: 2324 Offset :4

elim_double_block_8

elim_double_block_8  {
\find (          \modality{#allmodal}{.. { do #s while (#e); } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. do #s while (#e); ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "elim_double_block" 

};

defined in: javaRules.key Line: 2331 Offset :4

elim_double_block_9

elim_double_block_9  {
\find (          \modality{#allmodal}{.. { { #slist } { #slist1 } } ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. { #slist } { #slist1 } ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "elim_double_block" 

};

defined in: javaRules.key Line: 2338 Offset :4

remove_parentheses_right

remove_parentheses_right  {
\find (          \modality{#allmodal}{.. #lhs = (#e); ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = #e; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )

};

defined in: javaRules.key Line: 2349 Offset :4

remove_parentheses_attribute_left

remove_parentheses_attribute_left  {
\find (          \modality{#allmodal}{.. (#e.#attribute) = #e0; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #e.#attribute = #e0; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "remove_parentheses" 

};

defined in: javaRules.key Line: 2354 Offset :4

remove_parentheses_lhs_left

remove_parentheses_lhs_left  {
\find (          \modality{#allmodal}{.. (#lhs) = #e; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #lhs = #e; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "remove_parentheses" 

};

defined in: javaRules.key Line: 2360 Offset :4

compound_multiplication_1

compound_multiplication_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse * #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v * #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "multiplication" 

};

defined in: javaRules.key Line: 2370 Offset :4

compound_multiplication_2

compound_multiplication_2  {
\find (          \modality{#allmodal}{.. #lhs=#e * #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 * #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "multiplication" 

};

defined in: javaRules.key Line: 2378 Offset :4

compound_division_1

compound_division_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse / #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v / #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "division" 

};

defined in: javaRules.key Line: 2386 Offset :4

compound_division_2

compound_division_2  {
\find (          \modality{#allmodal}{.. #lhs=#e / #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 / #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "division" 

};

defined in: javaRules.key Line: 2394 Offset :4

compound_modulo_1

compound_modulo_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse % #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v % #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "modulo" 

};

defined in: javaRules.key Line: 2402 Offset :4

compound_modulo_2

compound_modulo_2  {
\find (          \modality{#allmodal}{.. #lhs=#e % #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 % #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "modulo" 

};

defined in: javaRules.key Line: 2410 Offset :4

compound_addition_1

compound_addition_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse + #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v + #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "addition" 

};

defined in: javaRules.key Line: 2418 Offset :4

compound_addition_2

compound_addition_2  {
\find (          \modality{#allmodal}{.. #lhs=#e + #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 + #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "addition" 

};

defined in: javaRules.key Line: 2426 Offset :4

compound_binary_AND_1

compound_binary_AND_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse & #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v & #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "binary_AND" 

};

defined in: javaRules.key Line: 2434 Offset :4

compound_binary_AND_2

compound_binary_AND_2  {
\find (          \modality{#allmodal}{.. #lhs=#e & #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 & #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "binary_AND" 

};

defined in: javaRules.key Line: 2442 Offset :4

compound_binary_OR_1

compound_binary_OR_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse | #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v | #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "binary_OR" 

};

defined in: javaRules.key Line: 2450 Offset :4

compound_binary_OR_2

compound_binary_OR_2  {
\find (          \modality{#allmodal}{.. #lhs=#e | #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 | #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "binary_OR" 

};

defined in: javaRules.key Line: 2458 Offset :4

compound_binary_XOR_1

compound_binary_XOR_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse ^ #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v ^ #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "binary_XOR" 

};

defined in: javaRules.key Line: 2466 Offset :4

compound_binary_XOR_2

compound_binary_XOR_2  {
\find (          \modality{#allmodal}{.. #lhs=#e ^ #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 ^ #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "binary_XOR" 

};

defined in: javaRules.key Line: 2474 Offset :4

compound_invert_bits

compound_invert_bits  {
\find (          \modality{#allmodal}{.. #lhs=~#nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..  #typeof(#nse) #v1=#nse; #lhs=~#v1 ; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "invert_bits" 

};

defined in: javaRules.key Line: 2482 Offset :4

compound_subtraction_1

compound_subtraction_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse - #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v - #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "subtraction" 

};

defined in: javaRules.key Line: 2490 Offset :4

compound_subtraction_2

compound_subtraction_2  {
\find (          \modality{#allmodal}{.. #lhs=#e - #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 - #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "subtraction" 

};

defined in: javaRules.key Line: 2498 Offset :4

compound_shiftright_1

compound_shiftright_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse >> #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v >> #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "shift" 

};

defined in: javaRules.key Line: 2506 Offset :4

compound_shiftright_2

compound_shiftright_2  {
\find (          \modality{#allmodal}{.. #lhs=#e >> #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 >> #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "shift" 

};

defined in: javaRules.key Line: 2514 Offset :4

compound_unsigned_shiftright_1

compound_unsigned_shiftright_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse >>> #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v >>> #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "shift" 

};

defined in: javaRules.key Line: 2522 Offset :4

compound_unsigned_shiftright_2

compound_unsigned_shiftright_2  {
\find (          \modality{#allmodal}{.. #lhs=#e >>> #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 >>> #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "shift" 

};

defined in: javaRules.key Line: 2530 Offset :4

compound_shiftleft_1

compound_shiftleft_1  {
\find (          \modality{#allmodal}{.. #lhs=#nse << #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse) #v=#nse; #lhs=#v << #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "shift" 

};

defined in: javaRules.key Line: 2538 Offset :4

compound_shiftleft_2

compound_shiftleft_2  {
\find (          \modality{#allmodal}{.. #lhs=#e << #nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse) #v1=#nse; #lhs=#v0 << #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "shift" 

};

defined in: javaRules.key Line: 2546 Offset :4

compound_equality_comparison_1

compound_equality_comparison_1  {
\find (          \modality{#allmodal}{.. #lhs = #nse0 == #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse0) #v0 = #nse0; #lhs = #v0 == #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "equality" 

};

defined in: javaRules.key Line: 2554 Offset :4

compound_equality_comparison_2

compound_equality_comparison_2  {
\find (          \modality{#allmodal}{.. #lhs = #e == #nse0; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse0) #v1 = #nse0; #lhs = #v0 == #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "equality" 

};

defined in: javaRules.key Line: 2562 Offset :4

compound_inequality_comparison_1

compound_inequality_comparison_1  {
\find (          \modality{#allmodal}{.. #lhs = #nse0 != #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse0) #v0 = #nse0; #lhs = #v0 != #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "inequality" 

};

defined in: javaRules.key Line: 2570 Offset :4

compound_inequality_comparison_2

compound_inequality_comparison_2  {
\find (          \modality{#allmodal}{.. #lhs = #e != #nse0; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse0) #v1 = #nse0; #lhs = #v0 != #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "inequality" 

};

defined in: javaRules.key Line: 2578 Offset :4

compound_less_than_comparison_1

compound_less_than_comparison_1  {
\find (          \modality{#allmodal}{.. #lhs = #nse0 < #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse0) #v0 = #nse0; #lhs = #v0 < #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "less_than" 

};

defined in: javaRules.key Line: 2586 Offset :4

compound_less_than_comparison_2

compound_less_than_comparison_2  {
\find (          \modality{#allmodal}{.. #lhs = #e < #nse0; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse0) #v1 = #nse0; #lhs = #v0 < #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "less_than" 

};

defined in: javaRules.key Line: 2594 Offset :4

compound_less_equal_than_comparison_1

compound_less_equal_than_comparison_1  {
\find (          \modality{#allmodal}{.. #lhs = #nse0 <= #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse0) #v0 = #nse0; #lhs = #v0 <= #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "less_or_equal" 

};

defined in: javaRules.key Line: 2602 Offset :4

compound_less_equal_than_comparison_2

compound_less_equal_than_comparison_2  {
\find (          \modality{#allmodal}{.. #lhs = #e <= #nse0; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse0) #v1 = #nse0; #lhs = #v0 <= #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "less_or_equal" 

};

defined in: javaRules.key Line: 2610 Offset :4

compound_greater_than_comparison_1

compound_greater_than_comparison_1  {
\find (          \modality{#allmodal}{.. #lhs = #nse0 > #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse0) #v0 = #nse0; #lhs = #v0 > #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "greater_than" 

};

defined in: javaRules.key Line: 2618 Offset :4

compound_greater_than_comparison_2

compound_greater_than_comparison_2  {
\find (          \modality{#allmodal}{.. #lhs = #e > #nse0; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse0) #v1 = #nse0; #lhs = #v0 > #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "greater_than" 

};

defined in: javaRules.key Line: 2626 Offset :4

compound_greater_equal_than_comparison_1

compound_greater_equal_than_comparison_1  {
\find (          \modality{#allmodal}{.. #lhs = #nse0 >= #se; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#nse0) #v0 = #nse0; #lhs = #v0 >= #se; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "greater_or_equal" 

};

defined in: javaRules.key Line: 2634 Offset :4

compound_greater_equal_than_comparison_2

compound_greater_equal_than_comparison_2  {
\find (          \modality{#allmodal}{.. #lhs = #e >= #nse0; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#e) #v0=#e; #typeof(#nse0) #v1 = #nse0; #lhs = #v0 >= #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog )
\displayname   "greater_or_equal" 

};

defined in: javaRules.key Line: 2642 Offset :4

compound_assignment_1_new

compound_assignment_1_new  {
\find (          \modality{#allmodal}{.. #lhs=!#seBool; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   #seBool=           TRUE )\then (                   FALSE )\else (                   TRUE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "assignment_negation" 

};

defined in: javaRules.key Line: 2657 Offset :4

compound_assignment_2

compound_assignment_2  {
\find (          \modality{#allmodal}{.. #lhs=!#nseBool; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. boolean #v=#nseBool; #lhs=!#v; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "compound_assignment" 

};

defined in: javaRules.key Line: 2664 Offset :4

compound_assignment_3_nonsimple

compound_assignment_3_nonsimple  {
\find (          \modality{#allmodal}{.. #lhs=#exBool0 && #nseBool1; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. if (!#exBool0) #lhs=false; else #lhs=#nseBool1; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression , split_if )
\displayname   "compound_assignment" 

};

defined in: javaRules.key Line: 2672 Offset :4

compound_assignment_3_mixed

compound_assignment_3_mixed  {
\find (          \modality{#allmodal}{.. #lhs=#nseBool0 && #seBool1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. boolean #v0 = #nseBool0; #lhs = #v0 && #seBool1; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "compound_assignment" 

};

defined in: javaRules.key Line: 2679 Offset :4

compound_assignment_3_simple

compound_assignment_3_simple  {
\find (          \modality{#allmodal}{.. #lhs=#seBool0 && #seBool1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   #seBool0=           TRUE )\then (                  \if (                   #seBool1=           TRUE )\then (                   TRUE )\else (                   FALSE ))\else (                   FALSE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "assignment_and" 

};

defined in: javaRules.key Line: 2687 Offset :4

compound_assignment_4_nonsimple

compound_assignment_4_nonsimple  {
\find (          \modality{#allmodal}{.. #lhs=#nseBool0 & #exBool1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. boolean #v0 = #nseBool0;
                boolean #v1 = #exBool1; #lhs= #v0 & #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "compound_assignment" 

};

defined in: javaRules.key Line: 2695 Offset :4

compound_assignment_4_simple

compound_assignment_4_simple  {
\find (          \modality{#allmodal}{.. #lhs=#seBool0 & #seBool1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   #seBool0=           TRUE )\then (                  \if (                   #seBool1=           TRUE )\then (                   TRUE )\else (                   FALSE ))\else (                   FALSE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "assignment_and" 

};

defined in: javaRules.key Line: 2704 Offset :4

compound_assignment_5_nonsimple

compound_assignment_5_nonsimple  {
\find (          \modality{#allmodal}{.. #lhs=#exBool0 || #nseBool1; ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. if (#exBool0) #lhs=true; else #lhs=#nseBool1; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression , split_if )
\displayname   "compound_assignment" 

};

defined in: javaRules.key Line: 2712 Offset :4

compound_assignment_5_mixed

compound_assignment_5_mixed  {
\find (          \modality{#allmodal}{.. #lhs=#nseBool0 || #seBool1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. boolean #v0 = #nseBool0; #lhs = #v0 || #seBool1; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "compound_assignment" 

};

defined in: javaRules.key Line: 2719 Offset :4

compound_assignment_5_simple

compound_assignment_5_simple  {
\find (          \modality{#allmodal}{.. #lhs=#seBool0 || #seBool1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   #seBool0=           TRUE )\then (                   TRUE )\else (                  \if (                   #seBool1=           TRUE )\then (                   TRUE )\else (                   FALSE ))} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "assignment_or" 

};

defined in: javaRules.key Line: 2727 Offset :4

compound_assignment_6_nonsimple

compound_assignment_6_nonsimple  {
\find (          \modality{#allmodal}{.. #lhs=#nseBool0 | #exBool1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. boolean #v0 = #nseBool0;
                boolean #v1 = #exBool1; #lhs = #v0 | #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "compound_assignment" 

};

defined in: javaRules.key Line: 2735 Offset :4

compound_assignment_6_simple

compound_assignment_6_simple  {
\find (          \modality{#allmodal}{.. #lhs=#seBool0 | #seBool1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   #seBool0=           TRUE )\then (                   TRUE )\else (                  \if (                   #seBool1=           TRUE )\then (                   TRUE )\else (                   FALSE ))} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "assignment_or" 

};

defined in: javaRules.key Line: 2744 Offset :4

compound_assignment_xor_nonsimple

compound_assignment_xor_nonsimple  {
\find (          \modality{#allmodal}{.. #lhs=#nseBool0 ^ #exBool1; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. boolean #v0 = #nseBool0;
                boolean #v1 = #exBool1; #lhs = #v0 ^ #v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "compound_assignment" 

};

defined in: javaRules.key Line: 2752 Offset :4

compound_assignment_xor_simple

compound_assignment_xor_simple  {
\find (          \modality{#allmodal}{.. #lhs=#seBool0 ^ #seBool1; ...}\endmodality            (                   post ))
  \replacewith (                {                  #lhs:=                \if (                   #seBool0=           #seBool1)\then (                   FALSE )\else (                   TRUE )} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_expression )
\displayname   "assignment_xor" 

};

defined in: javaRules.key Line: 2761 Offset :4

eval_order_array_access1

eval_order_array_access1  {
\find (          \modality{#allmodal}{..#nv[#e]=#e0;...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#nv) #v0=#nv;
                #v0[#e]=#e0;
                 ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentUnfoldLeft" 

};

defined in: javaRules.key Line: 2773 Offset :4

eval_order_array_access2

eval_order_array_access2  {
\find (          \modality{#allmodal}{..#v[#nse]=#e;...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#v) #ar1 = #v;
                #typeof(#nse) #v0=#nse;
                #ar1[#v0]=#e;
                     ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentUnfoldLeft" 

};

defined in: javaRules.key Line: 2783 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

eval_order_array_access3

eval_order_array_access3  {
\find (          \modality{#allmodal}{..#v[#se]=#nse;...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#v) #v0=#v;
                #typeof(#se) #v2=#se;
                #typeof(#nse) #v1=#nse;
                #v0[#v2]=#v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentSaveLocation" 

};

defined in: javaRules.key Line: 2796 Offset :4

Taclets

Enabled under choices: programRules:Java

eval_order_array_access3

eval_order_array_access3  {
\find (          \modality{#allmodal}{..#v[#se]=#nse;...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#v) #v0=#v;
                #typeof(#se) #v2=#se;
                #typeof(#nse) #v1=#nse;
                #v0[#v2]=#v1; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentSaveLocation" 

};

defined in: javaRules.key Line: 2810 Offset :4

eval_order_array_access4

eval_order_array_access4  {
\find (          \modality{#allmodal}{..#v=#nv[#e];...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#nv) #v0=#nv;
                #v=#v0[#e];
                    ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentUnfoldRight" 

};

defined in: javaRules.key Line: 2822 Offset :4

eval_order_array_access5

eval_order_array_access5  {
\find (          \modality{#allmodal}{..#v=#v0[#nse];...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#v0) #ar1 = #v0;
                #typeof(#nse) #v1=#nse;
                #v=#ar1[#v1];
                    ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentUnfoldRight" 

};

defined in: javaRules.key Line: 2832 Offset :4

eval_order_array_access6

eval_order_array_access6  {
\find (          \modality{#allmodal}{..#v=#nv.#length; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#nv) #v0=#nv; #v=#v0.#length; ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentUnfoldRight" 

};

defined in: javaRules.key Line: 2843 Offset :4

eval_order_access1

eval_order_access1  {
\find (          \modality{#allmodal}{..#nv.#attribute=#e;...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#nv) #v0=#nv; #v0.#attribute=#e;...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentUnfoldLeft" 

};

defined in: javaRules.key Line: 2854 Offset :4

eval_order_access2

eval_order_access2  {
\find (          \modality{#allmodal}{.. #v=#nv.#attribute; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..#typeof(#nv) #v0=#nv; #v=#v0.#attribute;...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentUnfoldRight" 

};

defined in: javaRules.key Line: 2862 Offset :4

eval_order_access4_this

eval_order_access4_this  {
\find (          \modality{#allmodal}{.. #v.#a=#nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..
                #typeof(#nse) #v1=#nse;
                #v.#a=#v1;...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentSaveLocationThis" 

};

defined in: javaRules.key Line: 2870 Offset :4

eval_order_access4

eval_order_access4  {
\find (          \modality{#allmodal}{.. #v.#a=#nse; ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#v) #v0=#v;
                #typeof(#nse) #v1=#nse;
                 #v0.#a=#v1;...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentSaveLocation" 

};

defined in: javaRules.key Line: 2882 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow

assignment_to_reference_array_component

assignment_to_reference_array_component  {
\schemaVar   \modalOperator  {  diamond ,  box } #normal;
\find (          \modality{#normal}{.. #v[#se]=#se0; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#v != null)" :  \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)} \modality{#normal}{.. ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&             lt   (                   #se,                    length   (                   #v))&             geq   (                   #se,                    0 )&             arrayStoreValid   (                   #v,                    #se0)==>  );
 (  permissions : on ) {
  "Write Permission to #v[#se]" :  \replacewith (          \modality{#normal}{.. assert false : "Access permission check-point (write)."; ...}\endmodality            (                   post )) \add (  ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    arr   (                   #se))))}
;
  "Null Reference (#v = null)" :  \replacewith (          \modality{#normal}{.. throw new java.lang.NullPointerException(); ...}\endmodality            (                   post )) \add (                     #v=           null ==>  );
  "Index Out of Bounds (#v != null, but #se Out of Bounds!)" :  \replacewith (          \modality{#normal}{.. throw new java.lang.ArrayIndexOutOfBoundsException(); ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&            (                   leq   (                   length   (                   #v),                    #se)|              lt   (                   #se,                    0 ))==>  );
  "Array Store Exception (incompatible dynamic element type of #v and #se0)" :  \replacewith (          \modality{#normal}{.. throw new java.lang.ArrayStoreException(); ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&             lt   (                   #se,                    length   (                   #v))&             geq   (                   #se,                    0 )&   !             arrayStoreValid   (                   #v,                    #se0)==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 2897 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow JavaCard:on

assignment_to_reference_array_component_transaction

assignment_to_reference_array_component_transaction  {
\schemaVar   \modalOperator  {  diamond_transaction ,  box_transaction } #transaction;
\find (          \modality{#transaction}{.. #v[#se]=#se0; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#v != null)" :  \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)}  {                  savedHeap :=                \if (                  int ::  select   (                   heap ,                    #v,                   java.lang.Object ::   )=           0 )\then (                   store   (                   savedHeap ,                    #v,                   java.lang.Object ::   ,                    TRUE ))\else (                  \if (                  boolean ::  select   (                   savedHeap ,                    #v,                   java.lang.Object ::   )=           FALSE )\then (                   store   (                   savedHeap ,                    #v,                    arr   (                   #se),                    #se0))\else (                   savedHeap ))} \modality{#transaction}{.. ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&             lt   (                   #se,                    length   (                   #v))&             geq   (                   #se,                    0 )&             arrayStoreValid   (                   #v,                    #se0)==>  );
  "Null Reference (#v = null)" :  \replacewith (          \modality{#transaction}{.. throw new java.lang.NullPointerException(); ...}\endmodality            (                   post )) \add (                     #v=           null ==>  );
  "Index Out of Bounds (#v != null, but #se Out of Bounds!)" :  \replacewith (          \modality{#transaction}{.. throw new java.lang.ArrayIndexOutOfBoundsException(); ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&            (                   leq   (                   length   (                   #v),                    #se)|              lt   (                   #se,                    0 ))==>  );
  "Array Store Exception (incompatible dynamic element type of #v and #se0)" :  \replacewith (          \modality{#transaction}{.. throw new java.lang.ArrayStoreException(); ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&             lt   (                   #se,                    length   (                   #v))&             geq   (                   #se,                    0 )&   !             arrayStoreValid   (                   #v,                    #se0)==>  )
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment_to_reference_array_component" 

};

defined in: javaRules.key Line: 2925 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban

assignment_to_reference_array_component

assignment_to_reference_array_component  {
\schemaVar   \modalOperator  {  diamond ,  box } #normal;
\find ( ==>           \modality{#normal}{.. #v[#se]=#se0; ...}\endmodality            (                   post ))
\varcond   "Normal Execution (#v != null)" :  \replacewith ( ==>                 {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)} \modality{#normal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Write Permission to #v[#se]" :  \replacewith ( ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    arr   (                   #se))))}
;
  "Null Reference (#v = null)" :  \replacewith ( ==>                     false ) \add (                     #v=           null ==>  );
  "Index Out of Bounds (#v != null, but #se Out of Bounds!)" :  \replacewith ( ==>                     false ) \add (           !            (                   #v=           null )&            (                   leq   (                   length   (                   #v),                    #se)|              lt   (                   #se,                    0 ))==>  );
  "Array Store Exception (incompatible dynamic element type of #v and #se0)" :  \replacewith ( ==>                     false ) \add (           !            (                   #v=           null )&             lt   (                   #se,                    length   (                   #v))&             geq   (                   #se,                    0 )&   !             arrayStoreValid   (                   #v,                    #se0)==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 2956 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

assignment_to_reference_array_component

assignment_to_reference_array_component  {
\schemaVar   \modalOperator  {  diamond ,  box } #normal;
\find (          \modality{#normal}{.. #v[#se]=#se0; ...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)} \modality{#normal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 2982 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban JavaCard:on

assignment_to_reference_array_component_transaction

assignment_to_reference_array_component_transaction  {
\schemaVar   \modalOperator  {  diamond_transaction ,  box_transaction } #transaction;
\find ( ==>           \modality{#transaction}{.. #v[#se]=#se0; ...}\endmodality            (                   post ))
\varcond   "Normal Execution (#v != null)" :  \replacewith ( ==>                 {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)}  {                  savedHeap :=                \if (                  int ::  select   (                   heap ,                    #v,                   java.lang.Object ::   )=           0 )\then (                   store   (                   savedHeap ,                    #v,                   java.lang.Object ::   ,                    TRUE ))\else (                  \if (                  boolean ::  select   (                   savedHeap ,                    #v,                   java.lang.Object ::   )=           FALSE )\then (                   store   (                   savedHeap ,                    #v,                    arr   (                   #se),                    #se0))\else (                   savedHeap ))} \modality{#transaction}{.. ...}\endmodality            (                   post ));
  "Null Reference (#v = null)" :  \replacewith ( ==>                     false ) \add (                     #v=           null ==>  );
  "Index Out of Bounds (#v != null, but #se Out of Bounds!)" :  \replacewith ( ==>                     false ) \add (           !            (                   #v=           null )&            (                   leq   (                   length   (                   #v),                    #se)|              lt   (                   #se,                    0 ))==>  );
  "Array Store Exception (incompatible dynamic element type of #v and #se0)" :  \replacewith ( ==>                     false ) \add (           !            (                   #v=           null )&             lt   (                   #se,                    length   (                   #v))&             geq   (                   #se,                    0 )&   !             arrayStoreValid   (                   #v,                    #se0)==>  )
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment_to_reference_array_component" 

};

defined in: javaRules.key Line: 2992 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore JavaCard:on

assignment_to_reference_array_component_transaction

assignment_to_reference_array_component_transaction  {
\schemaVar   \modalOperator  {  diamond_transaction ,  box_transaction } #transaction;
\find (          \modality{#transaction}{.. #v[#se]=#se0; ...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)}  {                  savedHeap :=                \if (                  int ::  select   (                   heap ,                    #v,                   java.lang.Object ::   )=           0 )\then (                   store   (                   savedHeap ,                    #v,                   java.lang.Object ::   ,                    TRUE ))\else (                  \if (                  boolean ::  select   (                   savedHeap ,                    #v,                   java.lang.Object ::   )=           FALSE )\then (                   store   (                   savedHeap ,                    #v,                    arr   (                   #se),                    #se0))\else (                   savedHeap ))} \modality{#transaction}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment_to_reference_array_component" 

};

defined in: javaRules.key Line: 3023 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow

assignment_to_primitive_array_component

assignment_to_primitive_array_component  {
\schemaVar   \modalOperator  {  diamond ,  box } #normal;
\find (          \modality{#normal}{..#v[#se]=#se0;...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#v != null)" :  \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)} \modality{#normal}{.. ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&             lt   (                   #se,                    length   (                   #v))&             geq   (                   #se,                    0 )==>  );
 (  permissions : on ) {
  "Write Permission to #v[#se]" :  \replacewith (          \modality{#normal}{.. assert false : "Access permission check-point (write)."; ...}\endmodality            (                   post )) \add (  ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    arr   (                   #se))))}
;
  "Null Reference (#v = null)" :  \replacewith (          \modality{#normal}{..
                    throw new java.lang.NullPointerException();
                    ...}\endmodality            (                   post )) \add (                     #v=           null ==>  );
  "Index Out of Bounds (#v != null, but #se Out of Bounds!)" :  \replacewith (          \modality{#normal}{.. throw new java.lang.ArrayIndexOutOfBoundsException(); ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&            (                   leq   (                   length   (                   #v),                    #se)|              lt   (                   #se,                    0 ))==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3042 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow JavaCard:on

assignment_to_primitive_array_component_transaction

assignment_to_primitive_array_component_transaction  {
\schemaVar   \modalOperator  {  diamond_transaction ,  box_transaction } #transaction;
\find (          \modality{#transaction}{..#v[#se]=#se0;...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#v != null)" :  \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)}  {                  savedHeap :=                \if (                  int ::  select   (                   heap ,                    #v,                   java.lang.Object ::   )=           0 )\then (                   store   (                   savedHeap ,                    #v,                   java.lang.Object ::   ,                    TRUE ))\else (                  \if (                  boolean ::  select   (                   savedHeap ,                    #v,                   java.lang.Object ::   )=           FALSE )\then (                   store   (                   savedHeap ,                    #v,                    arr   (                   #se),                    #se0))\else (                   savedHeap ))} \modality{#transaction}{.. ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&             lt   (                   #se,                    length   (                   #v))&             geq   (                   #se,                    0 )==>  );
  "Null Reference (#v = null)" :  \replacewith (          \modality{#transaction}{..
                    throw new java.lang.NullPointerException();
                    ...}\endmodality            (                   post )) \add (                     #v=           null ==>  );
  "Index Out of Bounds (#v != null, but #se Out of Bounds!)" :  \replacewith (          \modality{#transaction}{.. throw new java.lang.ArrayIndexOutOfBoundsException(); ...}\endmodality            (                   post )) \add (           !            (                   #v=           null )&            (                   leq   (                   length   (                   #v),                    #se)|              lt   (                   #se,                    0 ))==>  )
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment_to_primitive_array_component" 

};

defined in: javaRules.key Line: 3068 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban

assignment_to_primitive_array_component

assignment_to_primitive_array_component  {
\schemaVar   \modalOperator  {  diamond ,  box } #normal;
\find ( ==>           \modality{#normal}{..#v[#se]=#se0;...}\endmodality            (                   post ))
\varcond   "Normal Execution (#v != null)" :  \replacewith ( ==>                 {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)} \modality{#normal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Write Permission to #v[#se]" :  \replacewith ( ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    arr   (                   #se))))}
;
  "Null Reference (#v = null)" :  \replacewith ( ==>                     false ) \add (                     #v=           null ==>  );
  "Index Out of Bounds (#v != null, but #se Out of Bounds!)" :  \replacewith ( ==>                     false ) \add (           !            (                   #v=           null )&            (                   leq   (                   length   (                   #v),                    #se)|              lt   (                   #se,                    0 ))==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3098 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

assignment_to_primitive_array_component

assignment_to_primitive_array_component  {
\schemaVar   \modalOperator  {  diamond ,  box } #normal;
\find (          \modality{#normal}{..#v[#se]=#se0;...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)} \modality{#normal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3121 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban JavaCard:on

assignment_to_primitive_array_component_transaction

assignment_to_primitive_array_component_transaction  {
\schemaVar   \modalOperator  {  diamond_transaction ,  box_transaction } #transaction;
\find ( ==>           \modality{#transaction}{..#v[#se]=#se0;...}\endmodality            (                   post ))
\varcond   "Normal Execution (#v != null)" :  \replacewith ( ==>                 {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)}  {                  savedHeap :=                \if (                  int ::  select   (                   heap ,                    #v,                   java.lang.Object ::   )=           0 )\then (                   store   (                   savedHeap ,                    #v,                   java.lang.Object ::   ,                    TRUE ))\else (                  \if (                  boolean ::  select   (                   savedHeap ,                    #v,                   java.lang.Object ::   )=           FALSE )\then (                   store   (                   savedHeap ,                    #v,                    arr   (                   #se),                    #se0))\else (                   savedHeap ))} \modality{#transaction}{.. ...}\endmodality            (                   post ));
  "Null Reference (#v = null)" :  \replacewith ( ==>                     false ) \add (                     #v=           null ==>  );
  "Index Out of Bounds (#v != null, but #se Out of Bounds!)" :  \replacewith ( ==>                     false ) \add (           !            (                   #v=           null )&            (                   leq   (                   length   (                   #v),                    #se)|              lt   (                   #se,                    0 ))==>  )
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment_to_primitive_array_component" 

};

defined in: javaRules.key Line: 3131 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore JavaCard:on

assignment_to_primitive_array_component_transaction

assignment_to_primitive_array_component_transaction  {
\schemaVar   \modalOperator  {  diamond_transaction ,  box_transaction } #transaction;
\find (          \modality{#transaction}{..#v[#se]=#se0;...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    arr   (                   #se),                    #se0)}  {                  savedHeap :=                \if (                  int ::  select   (                   heap ,                    #v,                   java.lang.Object ::   )=           0 )\then (                   store   (                   savedHeap ,                    #v,                   java.lang.Object ::   ,                    TRUE ))\else (                  \if (                  boolean ::  select   (                   savedHeap ,                    #v,                   java.lang.Object ::   )=           FALSE )\then (                   store   (                   savedHeap ,                    #v,                    arr   (                   #se),                    #se0))\else (                   savedHeap ))} \modality{#transaction}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment_to_primitive_array_component" 

};

defined in: javaRules.key Line: 3160 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow

assignment_array2

assignment_array2  {
\find (          \modality{#allmodal}{.. #v = #v0[#se]; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#v0 != null)" :  \replacewith (                {                  #v:=                G ::  select   (                   heap ,                    #v0,                    arr   (                   #se))} \modality{#allmodal}{.. ...}\endmodality            (                   post )) \add (  ==>                    (                   #v0=           null )|              leq   (                   length   (                   #v0),                    #se)|              lt   (                   #se,                    0 ));
 (  permissions : on ) {
  "Read Permission to #v0[#se]" :  \replacewith (          \modality{#allmodal}{.. assert false : "Access permission check-point (read)."; ...}\endmodality            (                   post )) \add (  ==>                     readPermission   (                  Permission ::  select   (                   permissions ,                    #v0,                    arr   (                   #se))))}
;
  "Null Reference (#v0 = null)" :  \replacewith (          \modality{#allmodal}{..
                    throw new java.lang.NullPointerException();
                        ...}\endmodality            (                   post )) \add (                     #v0=           null ==>  );
  "Index Out of Bounds (#v0 != null, but #se Out of Bounds!)" :  \replacewith (          \modality{#allmodal}{..
                    throw new java.lang.ArrayIndexOutOfBoundsException();
                    ...}\endmodality            (                   post )) \add (           !            (                   #v0=           null )&            (                   leq   (                   length   (                   #v0),                    #se)|              lt   (                   #se,                    0 ))==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3180 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban

assignment_array2

assignment_array2  {
\find ( ==>           \modality{#allmodal}{.. #v = #v0[#se]; ...}\endmodality            (                   post ))
\varcond   "Normal Execution (#v0 != null)" :  \replacewith ( ==>                 {                  #v:=                G ::  select   (                   heap ,                    #v0,                    arr   (                   #se))} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Read Permission to #v0[#se]" :  \replacewith ( ==>                     readPermission   (                  Permission ::  select   (                   permissions ,                    #v0,                    arr   (                   #se))))}
;
  "Null Reference (#v0 = null)" :  \replacewith ( ==>                     false ) \add (                     #v0=           null ==>  );
  "Index Out of Bounds (#v0 != null, but #se Out of Bounds!)" :  \replacewith ( ==>                     false ) \add (           !            (                   #v0=           null )&            (                   leq   (                   length   (                   #v0),                    #se)|              lt   (                   #se,                    0 ))==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3207 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

assignment_array2

assignment_array2  {
\find (          \modality{#allmodal}{.. #v = #v0[#se]; ...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  #v:=                G ::  select   (                   heap ,                    #v0,                    arr   (                   #se))} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3229 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow

assignment_read_attribute

assignment_read_attribute  {
\find (          \modality{#allmodal}{.. #v0 = #v.#a; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#v != null)" :  \replacewith (                {                  #v0:=                G ::  select   (                   heap ,                    #v,                    #memberPVToField  (                   #a))} \modality{#allmodal}{.. ...}\endmodality            (                   post )) \add (  ==>                    (                   #v=           null ));
 (  permissions : on ) {
  "Read Permission to #v.#a" :  \replacewith (          \modality{#allmodal}{.. assert false : "Access permission check-point (read)."; ...}\endmodality            (                   post )) \add (  ==>                     readPermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #a))))}
;
  "Null Reference (#v = null)" :  \replacewith (          \modality{#allmodal}{..throw new java.lang.NullPointerException();...}\endmodality            (                   post )) \add (                     #v=           null ==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3238 Offset :4

assignment_read_attribute_this

assignment_read_attribute_this  {
\find (          \modality{#allmodal}{.. #v0 = #v.#a; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution" :  \replacewith (                {                  #v0:=                G ::  select   (                   heap ,                    #v,                    #memberPVToField  (                   #a))} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Read Permission to #v.#a" :  \replacewith (          \modality{#allmodal}{.. assert false : "Access permission check-point (read)."; ...}\endmodality            (                   post )) \add (  ==>                     readPermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #a))))}

\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3261 Offset :4

assignment_read_length

assignment_read_length  {
\find (          \modality{#allmodal}{.. #v0 = #v.#length; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#v != null)" :  \replacewith (                {                  #v0:=                 length   (                   #v)} \modality{#allmodal}{.. ...}\endmodality            (                   post )) \add (  ==>                    (                   #v=           null ));
  "Null Reference (#v = null)" :  \replacewith (          \modality{#allmodal}{..throw new java.lang.NullPointerException();...}\endmodality            (                   post )) \add (                     #v=           null ==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3281 Offset :4

Taclets

Enabled under choices: programRules:Java

assignment_read_length_this

assignment_read_length_this  {
\find (          \modality{#allmodal}{.. #v0 = #v.#length; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   \replacewith (                {                  #v0:=                 length   (                   #v)} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3297 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban

assignment_read_attribute

assignment_read_attribute  {
\find ( ==>           \modality{#allmodal}{.. #v0 = #v.#a; ...}\endmodality            (                   post ))
\varcond   "Normal Execution (#v != null)" :  \replacewith ( ==>                 {                  #v0:=                G ::  select   (                   heap ,                    #v,                    #memberPVToField  (                   #a))} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Read Permission to #v.#a" :  \replacewith ( ==>                     readPermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #a))))}
;
  "Null Reference (#v = null)" :  \replacewith ( ==>                     false ) \add (                     #v=           null ==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3308 Offset :4

assignment_read_attribute_this

assignment_read_attribute_this  {
\find ( ==>           \modality{#allmodal}{.. #v0 = #v.#a; ...}\endmodality            (                   post ))
\varcond   "Normal Execution" :  \replacewith ( ==>                 {                  #v0:=                G ::  select   (                   heap ,                    #v,                    #memberPVToField  (                   #a))} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Read Permission to #v.#a" :  \replacewith ( ==>                     readPermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #a))))}

\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3330 Offset :4

assignment_read_length

assignment_read_length  {
\find ( ==>           \modality{#allmodal}{.. #v0 = #v.#length; ...}\endmodality            (                   post ))
\varcond   "Normal Execution (#v != null)" :  \replacewith ( ==>                 {                  #v0:=                 length   (                   #v)} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
  "Null Reference (#v = null)" :  \replacewith ( ==>                     false ) \add (                     #v=           null ==>  )
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3348 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

assignment_read_attribute

assignment_read_attribute  {
\find (          \modality{#allmodal}{.. #v0 = #v.#a; ...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  #v0:=                G ::  select   (                   heap ,                    #v,                    #memberPVToField  (                   #a))} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3364 Offset :4

assignment_read_attribute_this

assignment_read_attribute_this  {
\find (          \modality{#allmodal}{.. #v0 = #v.#a; ...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  #v0:=                G ::  select   (                   heap ,                    #v,                    #memberPVToField  (                   #a))} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3376 Offset :4

assignment_read_length

assignment_read_length  {
\find (          \modality{#allmodal}{.. #v0 = #v.#length; ...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  #v0:=                 length   (                   #v)} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3388 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:allow

assignment_write_attribute

assignment_write_attribute  {
\find (          \modality{#allmodal}{.. #v.#a=#se; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution (#v != null)" :  \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    #memberPVToField  (                   #a),                    #se)} \modality{#allmodal}{.. ...}\endmodality            (                   post )) \add (  ==>                    (                   #v=           null ));
 (  permissions : on ) {
  "Write Permission to #v.#a" :  \replacewith (          \modality{#allmodal}{.. assert false : "Access permission check-point (write)."; ...}\endmodality            (                   post )) \add (  ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #a))))}
;
  "Null Reference (#v = null)" :  \replacewith (          \modality{#allmodal}{..throw new java.lang.NullPointerException();...}\endmodality            (                   post )) \add (                     #v=           null ==>  )
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment" 

};

defined in: javaRules.key Line: 3398 Offset :4

assignment_write_attribute_this

assignment_write_attribute_this  {
\find (          \modality{#allmodal}{.. #v.#a=#se; ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   "Normal Execution" :  \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    #memberPVToField  (                   #a),                    #se)} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Write Permission to #v.#a" :  \replacewith (          \modality{#allmodal}{.. assert false : "Access permission check-point (write)."; ...}\endmodality            (                   post )) \add (  ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #a))))}

\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentThis" 

};

defined in: javaRules.key Line: 3417 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ban

assignment_write_attribute

assignment_write_attribute  {
\find ( ==>           \modality{#allmodal}{.. #v.#a=#se; ...}\endmodality            (                   post ))
\varcond   "Normal Execution (#v != null)" :  \replacewith ( ==>                 {                  heap :=                 store   (                   heap ,                    #v,                    #memberPVToField  (                   #a),                    #se)} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Write Permission to #v.#a" :  \replacewith ( ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #a))))}
;
  "Null Reference (#v = null)" :  \replacewith ( ==>                     false ) \add (                     #v=           null ==>  )
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment" 

};

defined in: javaRules.key Line: 3437 Offset :4

assignment_write_attribute_this

assignment_write_attribute_this  {
\find ( ==>           \modality{#allmodal}{.. #v.#a=#se; ...}\endmodality            (                   post ))
\varcond   "Normal Execution" :  \replacewith ( ==>                 {                  heap :=                 store   (                   heap ,                    #v,                    #memberPVToField  (                   #a),                    #se)} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Write Permission to #v.#a" :  \replacewith ( ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #a))))}

\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignmentThis" 

};

defined in: javaRules.key Line: 3455 Offset :4

Taclets

Enabled under choices: programRules:Java runtimeExceptions:ignore

assignment_write_attribute

assignment_write_attribute  {
\find (          \modality{#allmodal}{.. #v.#a=#se; ...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    #memberPVToField  (                   #a),                    #se)} \modality{#allmodal}{.. ...}\endmodality            (                   post ))
\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment" 

};

defined in: javaRules.key Line: 3473 Offset :4

Taclets

Enabled under choices: programRules:Java

box_true

box_true  {
\find (          \modality{#box}{.. #s ...}\endmodality             true )
  \replacewith (                    true )
\heuristics  (modal_tautology )

};

defined in: javaRules.key Line: 3489 Offset :4

diamond_false

diamond_false  {
\find (          \modality{#diamond}{.. #s ...}\endmodality             false )
  \replacewith (                    false )
\heuristics  (modal_tautology )

};

defined in: javaRules.key Line: 3495 Offset :4

diamond_and_left

diamond_and_left  {
\find (          \modality{#diamond}{.. #s ...}\endmodality            (                   post &             post1 )==>  )
  \replacewith (          \modality{#diamond}{.. #s ...}\endmodality             post &   \modality{#diamond}{.. #s ...}\endmodality             post1 ==>  )

};

defined in: javaRules.key Line: 3501 Offset :4

box_and_left

box_and_left  {
\find (          \modality{#box}{.. #s ...}\endmodality            (                   post &             post1 )==>  )
  \replacewith (          \modality{#box}{.. #s ...}\endmodality             post &   \modality{#box}{.. #s ...}\endmodality             post1 ==>  )

};

defined in: javaRules.key Line: 3506 Offset :4

diamond_and_right

diamond_and_right  {
\find ( ==>           \modality{#diamond}{.. #s ...}\endmodality            (                   post &             post1 ))
  \replacewith ( ==>           \modality{#diamond}{.. #s ...}\endmodality             post );
  \replacewith ( ==>           \modality{#diamond}{.. #s ...}\endmodality             post1 )

};

defined in: javaRules.key Line: 3511 Offset :4

box_and_right

box_and_right  {
\find ( ==>           \modality{#box}{.. #s ...}\endmodality            (                   post &             post1 ))
  \replacewith ( ==>           \modality{#box}{.. #s ...}\endmodality             post );
  \replacewith ( ==>           \modality{#box}{.. #s ...}\endmodality             post1 )

};

defined in: javaRules.key Line: 3517 Offset :4

diamond_or_right

diamond_or_right  {
\find ( ==>           \modality{#diamond}{.. #s ...}\endmodality            (                   post |              post1 ))
  \replacewith ( ==>           \modality{#diamond}{.. #s ...}\endmodality             post |    \modality{#diamond}{.. #s ...}\endmodality             post1 )

};

defined in: javaRules.key Line: 3523 Offset :4

box_or_right

box_or_right  {
\find ( ==>           \modality{#box}{.. #s ...}\endmodality            (                   post |              post1 ))
  \replacewith ( ==>           \modality{#box}{.. #s ...}\endmodality             post |    \modality{#box}{.. #s ...}\endmodality             post1 )

};

defined in: javaRules.key Line: 3528 Offset :4

diamond_or_left

diamond_or_left  {
\find (          \modality{#diamond}{.. #s ...}\endmodality            (                   post |              post1 )==>  )
  \replacewith (          \modality{#diamond}{.. #s ...}\endmodality             post |    \modality{#diamond}{.. #s ...}\endmodality             post1 ==>  )

};

defined in: javaRules.key Line: 3533 Offset :4

box_or_left

box_or_left  {
\find (          \modality{#box}{.. #s ...}\endmodality            (                   post |              post1 )==>  )
  \replacewith (          \modality{#box}{.. #s ...}\endmodality             post |    \modality{#box}{.. #s ...}\endmodality             post1 ==>  )

};

defined in: javaRules.key Line: 3538 Offset :4

same_diamonds_right

same_diamonds_right  {
\assumes (  ==>           \<{#s}\>             post )
\find ( ==>           \<{#s}\>             post1 )
  \add (  ==>           \<{#s}\>            (                   post |              post1 ))

};

defined in: javaRules.key Line: 3545 Offset :4

same_diamonds_left

same_diamonds_left  {
\assumes (           \<{.. #s ...}\>             post ==>  )
\find (          \<{.. #s ...}\>             post1 ==>  )
  \add (           \<{.. #s ...}\>            (                   post &             post1 )==>  )

};

defined in: javaRules.key Line: 3551 Offset :4

same_boxes_right

same_boxes_right  {
\assumes (  ==>           \[{.. #s ...}\]             post )
\find ( ==>           \[{.. #s ...}\]             post1 )
  \add (  ==>           \[{.. #s ...}\]            (                   post |              post1 ))

};

defined in: javaRules.key Line: 3557 Offset :4

same_boxes_left

same_boxes_left  {
\assumes (           \[{.. #s ...}\]             post ==>  )
\find (          \[{.. #s ...}\]             post1 ==>  )
  \add (           \[{.. #s ...}\]            (                   post &             post1 )==>  )

};

defined in: javaRules.key Line: 3563 Offset :4

boxToDiamond

boxToDiamond  {
\find (          \[{.. #s ...}\]             post )
  \replacewith (          !   \<{.. #s ...}\>   !             post )
\heuristics  (boxDiamondConv )

};

defined in: javaRules.key Line: 3569 Offset :4

boxToDiamondTransaction

boxToDiamondTransaction  {
\find (          \box_transaction{.. #s ...}\endmodality             post )
  \replacewith (          !   \diamond_transaction{.. #s ...}\endmodality   !             post )
\heuristics  (boxDiamondConv )
\displayname   "boxToDiamond" 

};

defined in: javaRules.key Line: 3575 Offset :4

diamondToBox

diamondToBox  {
\find (          \<{.. #s ...}\>             post )
  \replacewith (          !   \[{.. #s ...}\]   !             post )
\heuristics  (boxDiamondConv )

};

defined in: javaRules.key Line: 3583 Offset :4

diamondToBoxTransaction

diamondToBoxTransaction  {
\find (          \diamond_transaction{.. #s ...}\endmodality             post )
  \replacewith (          !   \box_transaction{.. #s ...}\endmodality   !             post )
\heuristics  (boxDiamondConv )
\displayname   "diamondToBox" 

};

defined in: javaRules.key Line: 3589 Offset :4

diamond_split_termination

diamond_split_termination  {
\find (          \<{.. #s ...}\>             post )
  \replacewith (          \[{.. #s ...}\]             post &   \<{.. #s ...}\>             true )

};

defined in: javaRules.key Line: 3596 Offset :4

Taclets

Enabled under choices: programRules:Java

assignment_write_static_attribute

assignment_write_static_attribute  {
\find (          \modality{#allmodal}{.. @(#sv) = #se; ...}\endmodality            (                   post ))
  \replacewith (                {                  heap :=                 store   (                   heap ,                    null ,                    #memberPVToField  (                   #sv),                    #se)} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Write Permission to #sv" :  \replacewith (          \modality{#allmodal}{.. assert false : "Access permission check-point (static write)."; ...}\endmodality            (                   post )) \add (  ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    null ,                    #memberPVToField  (                   #sv))))}

\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "assignment" 

};

defined in: javaRules.key Line: 3608 Offset :4

assignment_write_static_attribute_with_variable_prefix

assignment_write_static_attribute_with_variable_prefix  {
\find (          \modality{#allmodal}{.. @(#v.#sv) = #se; ...}\endmodality            (                   post ))
  \replacewith (                {                  heap :=                 store   (                   heap ,                    #v,                    #memberPVToField  (                   #sv),                    #se)} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Write Permission to #v.#sv" :  \replacewith (          \modality{#allmodal}{.. assert false : "Access permission check-point (static write)."; ...}\endmodality            (                   post )) \add (  ==>                     writePermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #sv))))}

\heuristics  (simplify_prog , simplify_prog_subset )
\displayname   "active_attribute_access" 

};

defined in: javaRules.key Line: 3622 Offset :4

assignment_read_static_attribute

assignment_read_static_attribute  {
\find (          \modality{#allmodal}{.. #v0 = @(#sv); ...}\endmodality            (                   post ))
\sameUpdateLevel 
\varcond   \replacewith (                {                  #v0:=                G ::  select   (                   heap ,                    null ,                    #memberPVToField  (                   #sv))} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Read Permission to #sv" :  \replacewith (          \modality{#allmodal}{.. assert false : "Access permission check-point (static read)."; ...}\endmodality            (                   post )) \add (  ==>                     readPermission   (                  Permission ::  select   (                   permissions ,                    null ,                    #memberPVToField  (                   #sv))))}

\heuristics  (simplify_prog , simplify_prog_subset )

};

defined in: javaRules.key Line: 3635 Offset :4

assignment_read_static_attribute_with_variable_prefix

assignment_read_static_attribute_with_variable_prefix  {
\find (          \modality{#allmodal}{.. #loc = @(#v.#sv); ...}\endmodality            (                   post ))
\varcond   \replacewith (                {                  #loc:=                G ::  select   (                   heap ,                    #v,                    #memberPVToField  (                   #sv))} \modality{#allmodal}{.. ...}\endmodality            (                   post ));
 (  permissions : on ) {
  "Read Permission to #v.#sv" :  \replacewith (          \modality{#allmodal}{.. assert false : "Access permission check-point (static read)."; ...}\endmodality            (                   post )) \add (  ==>                     readPermission   (                  Permission ::  select   (                   permissions ,                    #v,                    #memberPVToField  (                   #sv))))}

\heuristics  (simplify_prog )
\displayname   "assignment" 

};

defined in: javaRules.key Line: 3650 Offset :4

Taclets

Enabled under choices: programRules:Java initialisation:disableStaticInitialisation

staticMethodCall

staticMethodCall  {
\find (          \modality{#allmodal}{.. #se.#mn(#elist); ...}\endmodality            (                   post ))
\varcond   "Normal Execution" :  \replacewith (          \modality{#allmodal}{..
                     #method-call(#v0, #se.#mn(#elist));
                    ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3671 Offset :4

staticMethodCallWithAssignment

staticMethodCallWithAssignment  {
\find (          \modality{#allmodal}{.. #lhs = #se.#mn(#elist); ...}\endmodality            (                   post ))
\varcond   "Normal Execution" :  \replacewith (          \modality{#allmodal}{..
                    #typeof(#lhs) #v0;
                          #method-call(#v0, #se.#mn(#elist));
                        #lhs = #v0;
                      ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3682 Offset :4

staticMethodCallStaticViaTypereference

staticMethodCallStaticViaTypereference  {
\find (          \modality{#allmodal}{.. #t.#mn(#elist); ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  #method-call(#t.#mn(#elist)); ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3695 Offset :4

staticMethodCallStaticWithAssignmentViaTypereference

staticMethodCallStaticWithAssignmentViaTypereference  {
\find (          \modality{#allmodal}{.. #lhs = #t.#mn(#elist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..  #typeof(#lhs) #v0;
                #method-call(#v0, #t.#mn(#elist));
                #lhs = #v0; ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3702 Offset :4

methodCallWithAssignmentWithinClass

methodCallWithAssignmentWithinClass  {
\find (          \modality{#allmodal}{.#ex.. #lhs=#mn(#elist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#lhs) #v0;
                   #method-call(#ex, #v0, #mn(#elist));
                   #lhs = #v0;
                ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3712 Offset :4

methodCallWithinClass

methodCallWithinClass  {
\find (          \modality{#allmodal}{.. #mn(#elist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..
                #method-call(#mn(#elist)); ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3723 Offset :4

Taclets

Enabled under choices: programRules:Java initialisation:enableStaticInitialisation

staticMethodCall

staticMethodCall  {
\find (          \modality{#allmodal}{.. #se.#mn(#elist); ...}\endmodality            (                   post ))
\varcond   "Normal Execution" :  \replacewith (          \modality{#allmodal}{..
                    #static-initialisation(#se.#mn(#elist));
                    #method-call(#v0, #se.#mn(#elist));
                    ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3735 Offset :4

staticMethodCallWithAssignment

staticMethodCallWithAssignment  {
\find (          \modality{#allmodal}{.. #lhs = #se.#mn(#elist); ...}\endmodality            (                  (                   post )))
\varcond   "Normal Execution" :  \replacewith (          \modality{#allmodal}{..
                    #static-initialisation(#se.#mn(#elist));
                    #typeof(#lhs) #v0;
                          #method-call(#v0, #se.#mn(#elist));
                        #lhs = #v0;
                      ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3747 Offset :4

staticMethodCallStaticViaTypereference

staticMethodCallStaticViaTypereference  {
\find (          \modality{#allmodal}{.. #t.#mn(#elist); ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{..  #static-initialisation(#t.#mn(#elist));
                #method-call(#t.#mn(#elist)); ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3761 Offset :4

staticMethodCallStaticWithAssignmentViaTypereference

staticMethodCallStaticWithAssignmentViaTypereference  {
\find (          \modality{#allmodal}{.. #lhs = #t.#mn(#elist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..  #static-initialisation(#t.#mn(#elist));
                #typeof(#lhs) #v0;
                    #method-call(#v0, #t.#mn(#elist));
                    #lhs = #v0; ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3769 Offset :4

methodCallWithAssignmentWithinClass

methodCallWithAssignmentWithinClass  {
\find (          \modality{#allmodal}{.#ex.. #lhs=#mn(#elist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #static-initialisation(#mn(#elist));
                #typeof(#lhs) #v0;
                            #method-call(#ex, #v0, #mn(#elist));
                            #lhs = #v0;
                         ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3780 Offset :4

methodCallWithinClass

methodCallWithinClass  {
\find (          \modality{#allmodal}{.#ex.. #mn(#elist); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..
                #static-initialisation(#mn(#elist));
                #method-call(#ex, #mn(#elist)); ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3792 Offset :4

passiveMethodCallWithinClass

passiveMethodCallWithinClass  {
\find (          \modality{#allmodal}{.#ex.. @(#mn(#elist)); ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #method-call(#ex, #mn(#elist)); ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3803 Offset :4

passiveMethodCallStatic

passiveMethodCallStatic  {
\find (          \modality{#allmodal}{.. @(#t.#mn(#elist)); ...}\endmodality            (                   post ))
  \replacewith (          \modality{#allmodal}{.. #method-call(#t.#mn(#elist)); ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3810 Offset :4

passiveMethodCallWithAssignmentWithinClass

passiveMethodCallWithAssignmentWithinClass  {
\find (          \modality{#allmodal}{.#ex.. #lhs=@(#mn(#elist)); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{.. #typeof(#lhs) #v0;
                     #method-call(#ex, #v0, #mn(#elist));
                     #lhs = #v0;
                ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3817 Offset :4

passiveMethodCallStaticWithAssignment

passiveMethodCallStaticWithAssignment  {
\find (          \modality{#allmodal}{.. #lhs = @(#t.#mn(#elist)); ...}\endmodality            (                   post ))
\varcond   \replacewith (          \modality{#allmodal}{..  #typeof(#lhs) #v0;
                           #method-call(#v0, #t.#mn(#elist));
                          #lhs = #v0;
                ...}\endmodality            (                   post ))
\heuristics  (method_expand )
\displayname   "methodCall" 

};

defined in: javaRules.key Line: 3828 Offset :4

Taclets

Enabled under choices: programRules:Java initialisation:enableStaticInitialisation

class_being_initialized_is_prepared

class_being_initialized_is_prepared  {
\assumes (                    boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   )=           TRUE ,                     wellFormed   (                   heap )==>  )
\find (                   boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   ))
\sameUpdateLevel 
  \replacewith (                    TRUE )
\heuristics  (confluence_restricted , simplify )
\displayname   "initialized classes have been prepared" 

};

defined in: javaRules.key Line: 3846 Offset :4

initialized_class_is_prepared

initialized_class_is_prepared  {
\assumes (                    boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   )=           TRUE ,                     wellFormed   (                   heap )==>  )
\find (                   boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   ))
\sameUpdateLevel 
  \replacewith (                    TRUE )
\heuristics  (confluence_restricted , simplify )
\displayname   "classes being initialized have been prepared" 

};

defined in: javaRules.key Line: 3855 Offset :4

initialized_class_is_not_erroneous

initialized_class_is_not_erroneous  {
\assumes (                    boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   )=           TRUE ,                     wellFormed   (                   heap )==>  )
\find (                   boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   ))
\sameUpdateLevel 
  \replacewith (                    FALSE )
\heuristics  (confluence_restricted , simplify )
\displayname   "initialized class is not erroneous" 

};

defined in: javaRules.key Line: 3864 Offset :4

class_initialized_excludes_class_init_in_progress

class_initialized_excludes_class_init_in_progress  {
\assumes (                    boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   )=           TRUE ,                     wellFormed   (                   heap )==>  )
\find (                   boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   ))
\sameUpdateLevel 
  \replacewith (                    FALSE )
\heuristics  (confluence_restricted , simplify )
\displayname   "initialisation process has already terminated" 

};

defined in: javaRules.key Line: 3873 Offset :4

class_erroneous_excludes_class_in_init

class_erroneous_excludes_class_in_init  {
\assumes (                    boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   )=           TRUE ,                     wellFormed   (                   heap )==>  )
\find (                   boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   ))
\sameUpdateLevel 
  \replacewith (                    FALSE )
\heuristics  (confluence_restricted , simplify )
\displayname   "initialization process has already terminated (or never begun)" 

};

defined in: javaRules.key Line: 3882 Offset :4

erroneous_class_has_no_initialized_sub_class

erroneous_class_has_no_initialized_sub_class  {
\assumes (                    boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   )=           TRUE ,                     wellFormed   (                   heap )==>  )
\find (                   boolean ::  select   (                   heap ,                    null ,                   betaObj ::   ))
\sameUpdateLevel 
\varcond   \replacewith (                    FALSE )
\heuristics  (confluence_restricted , simplify )
\displayname   "erroneous classes have no initialized subclasses" 

};

defined in: javaRules.key Line: 3891 Offset :4

superclasses_of_initialized_classes_are_initialized

superclasses_of_initialized_classes_are_initialized  {
\assumes (                    boolean ::  select   (                   heap ,                    null ,                   betaObj ::   )=           TRUE ,                     wellFormed   (                   heap )==>  )
\find (                   boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   ))
\sameUpdateLevel 
\varcond   \replacewith (                    TRUE )
\heuristics  (simplify )

};

defined in: javaRules.key Line: 3901 Offset :4

superclasses_of_initialized_classes_are_prepared

superclasses_of_initialized_classes_are_prepared  {
\assumes (                    boolean ::  select   (                   heap ,                    null ,                   betaObj ::   )=           TRUE ,                     wellFormed   (                   heap )==>  )
\find (                   boolean ::  select   (                   heap ,                    null ,                   alphaObj ::   ))
\sameUpdateLevel 
\varcond   \replacewith (                    TRUE )
\heuristics  (simplify )

};

defined in: javaRules.key Line: 3910 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview

javaRules.key

Taclets

getJavaCardTransient

setJavaCardTransient

beginJavaCardTransactionAPI

commitJavaCardTransactionAPI

abortJavaCardTransactionAPI

beginJavaCardTransactionDiamond

beginJavaCardTransactionBox

commitJavaCardTransactionDiamond

commitJavaCardTransactionBox

finishJavaCardTransactionDiamond

finishJavaCardTransactionBox

abortJavaCardTransactionDiamond

abortJavaCardTransactionBox

Taclets

emptyModality

emptyModalityBoxTransaction

emptyModalityDiamondTransaction

returnUnfold

deleteMergePoint

assignment

Taclets

assignment_write_array_this_access_normalassign

Taclets

assignment_write_array_this_access_normalassign

Taclets

eval_array_this_access

array_self_reference

array_self_reference_eq

null_can_always_be_stored_in_a_reference_type_array

array_store_known_dynamic_array_type

variableDeclaration

variableDeclarationFinal

variableDeclarationGhost

variableDeclarationAssign

variableDeclarationFinalAssign

variableDeclarationGhostAssign

variableDeclarationMult

array_post_declaration

throwNull

throwUnfold

throwLabel

throwLabelBlock

throwBox

throwDiamond

tryCatchThrow

tryMultipleCatchThrow

tryCatchFinallyThrow

tryFinallyThrow

tryEmpty

tryFinallyEmpty

tryBreakLabel

tryFinallyBreakLabel

tryBreak

tryFinallyBreak

try_continue_1

try_finally_continue_1

try_continue_2

try_finally_continue_2

tryReturn

tryFinallyReturn

tryReturnNoValue

tryFinallyReturnNoValue

preincrement_assignment

preincrement_assignment_attribute

preincrement_assignment_array

preincrement

preincrement_attribute

preincrement_array

predecrement

predecrement_attribute

predecrement_array

predecrement_assignment

predecrement_assignment_attribute

predecrement_assignment_array

postincrement_assignment