\generic G;defined in: instanceAllocation.key Line: 6 Offset :4\generic H \extends Object ;defined in: instanceAllocation.key Line: 7 Offset :4\generic J \extends Object ;defined in: instanceAllocation.key Line: 8 Offset :4\generic K;defined in: instanceAllocation.key Line: 9 Offset :4\generic alphaObj \extends Object ;defined in: instanceAllocation.key Line: 10 Offset :4\generic betaObj \extends Object ;defined in: instanceAllocation.key Line: 11 Offset :4instanceCreationUnfoldArguments {
\find ( \modality{#allmodal}{.. #nsn ...}\endmodality ( post ) )
\replacewith ( \modality{#allmodal}{.. #evaluate-arguments(#nsn); ...}\endmodality ( post ) )
\heuristics (simplify_autoname )
};defined in: instanceAllocation.key Line: 62 Offset :4instanceCreationAssignmentUnfoldArguments {
\find ( \modality{#allmodal}{.. #lhs = #nsn; ...}\endmodality ( post ) )
\replacewith ( \modality{#allmodal}{.. #evaluate-arguments(#lhs = #nsn); ...}\endmodality ( post ) )
\heuristics (simplify_autoname )
};defined in: instanceAllocation.key Line: 68 Offset :4instanceCreation {
\find ( \modality{#allmodal}{.. #n ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{.. #typeof(#v0) #v0 = #create-object(#n);
#constructor-call(#v0, #n);
#post-work(#v0); ...}\endmodality ( post ) )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 74 Offset :4instanceCreationAssignment {
\schemaVar \modalOperator { diamond , box } #normal ;
\find ( \modality{#normal}{.. #lhs = #n; ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#normal}{.. #typeof(#v0) #v0 = #create-object(#n);
#constructor-call(#v0, #n);
#post-work(#v0);
#lhs = #v0;
...}\endmodality ( post ) )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 83 Offset :4allocateInstance {
\find ( ==> \modality{#allmodal}{.#pm@#t2().. #lhs = #t.#allocate()@#t; ...}\endmodality ( post ) )
\varcond \replacewith ( ==> { heap := create ( heap , #lhs ) || permissions := create ( permissions , #lhs ) } \modality{#allmodal}{.. ...}\endmodality ( post ) ) \add ( #lhs != null & ( wellFormed ( heap ) -> select <[ boolean ]> ( heap , #lhs , java.lang.Object #$created ) = FALSE ) & ( wellFormed ( permissions ) -> select <[ boolean ]> ( permissions , #lhs , java.lang.Object #$created ) = FALSE ) & exactInstance <[ alphaObj ]> ( #lhs ) = TRUE ==> )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 98 Offset :4allocateInstanceWithLength {
\find ( ==> \modality{#allmodal}{.#pm@#t2().. #lhs = #t.#allocate(#len)@#t; ...}\endmodality ( post ) )
\varcond \replacewith ( ==> { heap := store ( store ( create ( heap , #lhs ) , #lhs , java.lang.Object #$transient , 0 ) , #lhs , java.lang.Object #$transactionConditionallyUpdated , FALSE ) || permissions := create ( permissions , #lhs ) } \modality{#allmodal}{.. ...}\endmodality ( post ) ) \add ( #lhs != null & ( wellFormed ( heap ) -> ( select <[ boolean ]> ( heap , #lhs , java.lang.Object #$created ) = FALSE & length ( #lhs ) = #len ) ) & ( wellFormed ( permissions ) -> select <[ boolean ]> ( permissions , #lhs , java.lang.Object #$created ) = FALSE ) & exactInstance <[ alphaObj ]> ( #lhs ) = TRUE ==> )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 115 Offset :4allocateInstance {
\find ( ==> \modality{#allmodal}{.#pm@#t2().. #lhs = #t.#allocate()@#t; ...}\endmodality ( post ) )
\varcond \replacewith ( ==> { heap := create ( heap , #lhs ) } \modality{#allmodal}{.. ...}\endmodality ( post ) ) \add ( #lhs != null & ( wellFormed ( heap ) -> select <[ boolean ]> ( heap , #lhs , java.lang.Object #$created ) = FALSE ) & exactInstance <[ alphaObj ]> ( #lhs ) = TRUE ==> )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 138 Offset :4allocateInstanceWithLength {
\find ( ==> \modality{#allmodal}{.#pm@#t2().. #lhs = #t.#allocate(#len)@#t; ...}\endmodality ( post ) )
\varcond \replacewith ( ==> { heap := store ( store ( create ( heap , #lhs ) , #lhs , java.lang.Object #$transient , 0 ) , #lhs , java.lang.Object #$transactionConditionallyUpdated , FALSE ) } \modality{#allmodal}{.. ...}\endmodality ( post ) ) \add ( #lhs != null & ( wellFormed ( heap ) -> ( select <[ boolean ]> ( heap , #lhs , java.lang.Object #$created ) = FALSE & length ( #lhs ) = #len ) ) & exactInstance <[ alphaObj ]> ( #lhs ) = TRUE ==> )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 150 Offset :4special_constructor_call {
\find ( \modality{#allmodal}{.. #scr ...}\endmodality ( post ) )
\replacewith ( \modality{#allmodal}{.. #special-constructor-call(#scr); ...}\endmodality ( post ) )
\heuristics (method_expand )
};defined in: instanceAllocation.key Line: 171 Offset :4arrayCreation {
\schemaVar \modalOperator { diamond , box } #normal ;
\find ( \modality{#normal}{.. #lhs = #na; ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#normal}{..
#typeof(#na) #v0;
#init-array-creation(#v0, #na);
#lhs = #v0; ...}\endmodality ( post ) )
\heuristics (simplify_prog )
};defined in: instanceAllocation.key Line: 182 Offset :4arrayCreationWithInitializers {
\find ( \modality{#allmodal}{.. #lhs = #arrayinitializer; ...}\endmodality ( post ) )
\varcond \replacewith ( \modality{#allmodal}{..
#typeof(#lhs) #v0;
#init-array-creation(#v0, #arrayinitializer);
#lhs = #v0; ...}\endmodality ( post ) )
\heuristics (simplify_prog )
};defined in: instanceAllocation.key Line: 193 Offset :4exact_instance_for_interfaces_or_abstract_classes {
\find ( exactInstance <[ G ]> ( obj ) )
\varcond \replacewith ( FALSE )
\heuristics (simplify )
\displayname "interfaces or abstract classes have no exact instances"
};defined in: instanceAllocation.key Line: 234 Offset :4