assignableDefinition {
\schemaVar \term Heap heapOld ;
\schemaVar \term Heap heapNew ;
\schemaVar \term LocSet locs ;
\schemaVar \variables Field f ;
\schemaVar \variables java.lang.Object o ;
\find ( assignable ( heapNew , heapOld , locs ) )
\varcond \replacewith ( \forall f ; ( \forall o ; ( elementOf ( o , f , locs ) | ! o = null & ! select <[ boolean ]> ( heapOld , o , java.lang.Object #$created ) = TRUE | select <[ any ]> ( heapNew , o , f ) = select <[ any ]> ( heapOld , o , f ) ) ) )
\heuristics (delayedExpansion )
};defined in: heapRules.key Line: 11 Offset :4selectOfStore {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\schemaVar \term alpha x ;
\find ( select <[ beta ]> ( store ( h , o , f , x ) , o2 , f2 ) )
\replacewith ( \if ( o = o2 & f = f2 & f != java.lang.Object #$created ) \then ( ( beta ) x ) \else ( select <[ beta ]> ( h , o2 , f2 ) ) )
\heuristics (semantics_blasting )
};defined in: heapRules.key Line: 37 Offset :4selectOfCreate {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f ;
\find ( select <[ beta ]> ( create ( h , o ) , o2 , f ) )
( permissions : off ) {
\replacewith ( \if ( o = o2 & o != null & f = java.lang.Object #$created ) \then ( ( beta ) TRUE ) \else ( select <[ beta ]> ( h , o2 , f ) ) ) }
;
( permissions : on ) {
\replacewith ( \if ( o = o2 & o != null ) \then ( \if ( f = java.lang.Object #$created ) \then ( ( beta ) TRUE ) \else ( defaultValue <[ beta ]> ) ) \else ( select <[ beta ]> ( h , o2 , f ) ) ) }
\heuristics (semantics_blasting )
};defined in: heapRules.key Line: 51 Offset :4selectOfAnon {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( select <[ beta ]> ( anon ( h , s , h2 ) , o , f ) )
\replacewith ( \if ( elementOf ( o , f , s ) & f != java.lang.Object #$created | elementOf ( o , f , freshLocs ( h ) ) ) \then ( select <[ beta ]> ( h2 , o , f ) ) \else ( select <[ beta ]> ( h , o , f ) ) )
\heuristics (semantics_blasting )
};defined in: heapRules.key Line: 74 Offset :4selectOfMemset {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term any x ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( select <[ beta ]> ( memset ( h , s , x ) , o , f ) )
\replacewith ( \if ( elementOf ( o , f , s ) & f != java.lang.Object #$created ) \then ( ( beta ) x ) \else ( select <[ beta ]> ( h , o , f ) ) )
\heuristics (semantics_blasting )
};defined in: heapRules.key Line: 89 Offset :4selectOfStoreEQ {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\schemaVar \term alpha x ;
\schemaVar \term Heap EQ ;
\assumes ( store ( h , o , f , x ) = EQ ==> )
\find ( select <[ beta ]> ( EQ , o2 , f2 ) )
\replacewith ( \if ( o = o2 & f = f2 & f != java.lang.Object #$created ) \then ( ( beta ) x ) \else ( select <[ beta ]> ( h , o2 , f2 ) ) )
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 124 Offset :4selectOfCreateEQ {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f ;
\schemaVar \term Heap EQ ;
\assumes ( create ( h , o ) = EQ ==> )
\find ( select <[ beta ]> ( EQ , o2 , f ) )
( permissions : off ) {
\replacewith ( \if ( o = o2 & o != null & f = java.lang.Object #$created ) \then ( ( beta ) TRUE ) \else ( select <[ beta ]> ( h , o2 , f ) ) ) }
;
( permissions : on ) {
\replacewith ( \if ( o = o2 & o != null ) \then ( \if ( f = java.lang.Object #$created ) \then ( ( beta ) TRUE ) \else ( defaultValue <[ beta ]> ) ) \else ( select <[ beta ]> ( h , o2 , f ) ) ) }
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 141 Offset :4selectOfAnonEQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap EQ ;
\assumes ( anon ( h , s , h2 ) = EQ ==> )
\find ( select <[ beta ]> ( EQ , o , f ) )
\replacewith ( \if ( elementOf ( o , f , s ) & f != java.lang.Object #$created | elementOf ( o , f , freshLocs ( h ) ) ) \then ( select <[ beta ]> ( h2 , o , f ) ) \else ( select <[ beta ]> ( h , o , f ) ) )
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 164 Offset :4selectOfMemsetEQ {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term any x ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap EQ ;
\assumes ( memset ( h , s , x ) = EQ ==> )
\find ( select <[ beta ]> ( EQ , o , f ) )
\replacewith ( \if ( elementOf ( o , f , s ) & f != java.lang.Object #$created ) \then ( ( beta ) x ) \else ( select <[ beta ]> ( h , o , f ) ) )
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 182 Offset :4pullOutSelect {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \skolemTerm beta selectSK ;
\find ( select <[ beta ]> ( h , o , f ) )
\replacewith ( selectSK << selectSK >> ) \add ( select <[ beta ]> ( h , o , f ) = selectSK << selectSK >> ==> )
\heuristics (pull_out_select )
};defined in: heapRules.key Line: 330 Offset :4simplifySelectOfStore {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\schemaVar \term alpha x ;
\schemaVar \term beta sk ;
\find ( select <[ beta ]> ( store ( h , o , f , x ) , o2 , f2 ) = sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( o = o2 & f = f2 & f != java.lang.Object #$created ) \then ( ( beta ) x ) \else ( select <[ beta ]> ( h , o2 , f2 ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( store ( h , o , f , x ) , o2 , f2 ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 343 Offset :4simplifySelectOfStoreEQ {
\schemaVar \term Heap h , EQ ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\schemaVar \term alpha x ;
\schemaVar \term beta sk ;
\assumes ( store ( h , o , f , x ) = EQ ==> )
\find ( select <[ beta ]> ( EQ , o2 , f2 ) = sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( o = o2 & f = f2 & f != java.lang.Object #$created ) \then ( ( beta ) x ) \else ( select <[ beta ]> ( h , o2 , f2 ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( EQ , o2 , f2 ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 370 Offset :4simplifySelectOfCreate {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f ;
\schemaVar \term beta sk ;
\find ( select <[ beta ]> ( create ( h , o ) , o2 , f ) = sk ==> )
\inSequentState
\inSequentState
( permissions : off ) {
\replacewith ( \if ( o = o2 & o != null & f = java.lang.Object #$created ) \then ( ( beta ) TRUE ) \else ( select <[ beta ]> ( h , o2 , f ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( create ( h , o ) , o2 , f ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};) }
;
( permissions : on ) {
\replacewith ( \if ( o = o2 & o != null ) \then ( \if ( f = java.lang.Object #$created ) \then ( ( beta ) TRUE ) \else ( defaultValue <[ beta ]> ) ) \else ( select <[ beta ]> ( h , o2 , f ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( create ( h , o ) , o2 , f ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};) }
\heuristics (simplify_select )
};defined in: heapRules.key Line: 398 Offset :4simplifySelectOfCreateEQ {
\schemaVar \term Heap h , EQ ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f ;
\schemaVar \term beta sk ;
\assumes ( create ( h , o ) = EQ ==> )
\find ( select <[ beta ]> ( EQ , o2 , f ) = sk ==> )
\inSequentState
\inSequentState
( permissions : off ) {
\replacewith ( \if ( o = o2 & o != null & f = java.lang.Object #$created ) \then ( ( beta ) TRUE ) \else ( select <[ beta ]> ( h , o2 , f ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( EQ , o2 , f ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};) }
;
( permissions : on ) {
\replacewith ( \if ( o = o2 & o != null ) \then ( \if ( f = java.lang.Object #$created ) \then ( ( beta ) TRUE ) \else ( defaultValue <[ beta ]> ) ) \else ( select <[ beta ]> ( h , o2 , f ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( EQ , o2 , f ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};) }
\heuristics (simplify_select )
};defined in: heapRules.key Line: 439 Offset :4simplifySelectOfAnon {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term beta sk ;
\find ( select <[ beta ]> ( anon ( h , s , h2 ) , o , f ) = sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( elementOf ( o , f , s ) & f != java.lang.Object #$created | elementOf ( o , f , freshLocs ( h ) ) ) \then ( select <[ beta ]> ( h2 , o , f ) ) \else ( select <[ beta ]> ( h , o , f ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( anon ( h , s , h2 ) , o , f ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 481 Offset :4simplifySelectOfAnonEQ {
\schemaVar \term Heap h , h2 , EQ ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term beta sk ;
\assumes ( anon ( h , s , h2 ) = EQ ==> )
\find ( select <[ beta ]> ( EQ , o , f ) = sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( elementOf ( o , f , s ) & f != java.lang.Object #$created | elementOf ( o , f , freshLocs ( h ) ) ) \then ( select <[ beta ]> ( h2 , o , f ) ) \else ( select <[ beta ]> ( h , o , f ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( EQ , o , f ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 509 Offset :4simplifySelectOfMemset {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term any x ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term beta sk ;
\find ( select <[ beta ]> ( memset ( h , s , x ) , o , f ) = sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( elementOf ( o , f , s ) & f != java.lang.Object #$created ) \then ( ( beta ) x ) \else ( select <[ beta ]> ( h , o , f ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( memset ( h , s , x ) , o , f ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 538 Offset :4simplifySelectOfMemsetEQ {
\schemaVar \term Heap h , EQ ;
\schemaVar \term LocSet s ;
\schemaVar \term any x ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term beta sk ;
\assumes ( memset ( h , s , x ) = EQ ==> )
\find ( select <[ beta ]> ( EQ , o , f ) = sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( elementOf ( o , f , s ) & f != java.lang.Object #$created ) \then ( ( beta ) x ) \else ( select <[ beta ]> ( h , o , f ) ) = sk ==> ) \addrules ( replaceKnownSelect {
\find ( select <[ beta ]> ( EQ , o , f ) )
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 566 Offset :4hideAuxiliaryEq {
\schemaVar \term any result , auxiliarySK ;
\find ( result = auxiliarySK ==> )
\inSequentState
\inSequentState
\replacewith ( ==> ) \addrules ( replaceKnownAuxiliaryConstant {
\find ( auxiliarySK )
\inSequentState
\inSequentState
\replacewith ( result )
\heuristics (concrete )
};)
\heuristics (hide_auxiliary_eq )
};defined in: heapRules.key Line: 599 Offset :4hideAuxiliaryEqConcrete {
\schemaVar \term any auxiliarySK ;
\find ( auxiliarySK = TRUE ==> )
\inSequentState
\inSequentState
\replacewith ( ==> ) \addrules ( replaceKnownAuxiliaryConstant {
\find ( auxiliarySK )
\inSequentState
\inSequentState
\replacewith ( TRUE )
\heuristics (concrete )
};)
\heuristics (hide_auxiliary_eq_const )
};defined in: heapRules.key Line: 614 Offset :4hideAuxiliaryEqConcrete2 {
\schemaVar \term any auxiliarySK ;
\find ( ==> auxiliarySK = TRUE )
\inSequentState
\inSequentState
\replacewith ( ==> ) \addrules ( replaceKnownAuxiliaryConstant {
\find ( auxiliarySK )
\inSequentState
\inSequentState
\replacewith ( FALSE )
\heuristics (concrete )
};)
\heuristics (hide_auxiliary_eq_const )
};defined in: heapRules.key Line: 629 Offset :4dismissNonSelectedField {
\schemaVar \term Heap h ;
\schemaVar \term Object o , u ;
\schemaVar \term Field f1 , f2 ;
\schemaVar \term any x ;
\find ( select <[ alpha ]> ( store ( h , o , f1 , x ) , u , f2 ) )
\varcond \replacewith ( select <[ alpha ]> ( h , u , f2 ) )
\heuristics (simplify )
};defined in: heapRules.key Line: 652 Offset :4dismissNonSelectedFieldEQ {
\schemaVar \term Heap h , EQ ;
\schemaVar \term Object o , u ;
\schemaVar \term Field f1 , f2 ;
\schemaVar \term any x ;
\assumes ( store ( h , o , f1 , x ) = EQ ==> )
\find ( select <[ alpha ]> ( EQ , u , f2 ) )
\varcond \replacewith ( select <[ alpha ]> ( h , u , f2 ) )
\heuristics (simplify )
};defined in: heapRules.key Line: 667 Offset :4dropEffectlessStores {
\schemaVar \term Heap h , result ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term any x ;
\find ( store ( h , o , f , x ) )
\varcond \replacewith ( result )
\heuristics (concrete )
};defined in: heapRules.key Line: 682 Offset :4memsetEmpty {
\schemaVar \term Heap h ;
\schemaVar \term any x ;
\find ( memset ( h , empty , x ) )
\replacewith ( h )
\heuristics (concrete )
};defined in: heapRules.key Line: 696 Offset :4selectCreatedOfAnon {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\find ( select <[ boolean ]> ( anon ( h , s , h2 ) , o , java.lang.Object #$created ) )
\replacewith ( \if ( select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE ) \then ( TRUE ) \else ( select <[ boolean ]> ( h2 , o , java.lang.Object #$created ) ) )
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 729 Offset :4selectCreatedOfAnonAsFormula {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\find ( select <[ boolean ]> ( anon ( h , s , h2 ) , o , java.lang.Object #$created ) = TRUE )
\replacewith ( select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE | select <[ boolean ]> ( h2 , o , java.lang.Object #$created ) = TRUE )
\heuristics (simplify_ENLARGING )
};defined in: heapRules.key Line: 744 Offset :4selectCreatedOfAnonEQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Heap EQ ;
\assumes ( anon ( h , s , h2 ) = EQ ==> )
\find ( select <[ boolean ]> ( EQ , o , java.lang.Object #$created ) )
\replacewith ( \if ( select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE ) \then ( TRUE ) \else ( select <[ boolean ]> ( h2 , o , java.lang.Object #$created ) ) )
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 758 Offset :4selectCreatedOfAnonAsFormulaEQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Heap EQ ;
\assumes ( anon ( h , s , h2 ) = EQ ==> )
\find ( select <[ boolean ]> ( EQ , o , java.lang.Object #$created ) = TRUE )
\replacewith ( select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE | select <[ boolean ]> ( h2 , o , java.lang.Object #$created ) = TRUE )
\heuristics (simplify_ENLARGING )
};defined in: heapRules.key Line: 775 Offset :4equalityToSelect {
\schemaVar \term Heap h , h2 ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\find ( h = h2 )
\varcond \replacewith ( \forall ov ; \forall fv ; ( select <[ any ]> ( h , ov , fv ) = select <[ any ]> ( h2 , ov , fv ) ) )
\heuristics (semantics_blasting )
};defined in: heapRules.key Line: 790 Offset :4onlyCreatedObjectsAreReferenced {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( wellFormed ( h ) ==> )
\find ( select <[ deltaObject ]> ( h , o , f ) )
\add ( select <[ deltaObject ]> ( h , o , f ) = null | select <[ boolean ]> ( h , select <[ deltaObject ]> ( h , o , f ) , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 808 Offset :4onlyCreatedObjectsAreReferencedFinal {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( wellFormed ( h ) , select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE ==> )
\find ( final <[ deltaObject ]> ( o , f ) )
\add ( final <[ deltaObject ]> ( o , f ) = null | select <[ boolean ]> ( h , final <[ deltaObject ]> ( o , f ) , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 824 Offset :4onlyCreatedObjectsAreInLocSets {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\assumes ( wellFormed ( h ) ==> )
\find ( elementOf ( o2 , f2 , select <[ LocSet ]> ( h , o , f ) ) ==> )
\add ( o2 = null | select <[ boolean ]> ( h , o2 , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 842 Offset :4onlyCreatedObjectsAreInLocSetsFinal {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\assumes ( wellFormed ( h ) ==> )
\find ( elementOf ( o2 , f2 , final <[ LocSet ]> ( o , f ) ) ==> )
\add ( o2 = null | select <[ boolean ]> ( h , o2 , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 858 Offset :4onlyCreatedObjectsAreInLocSetsEQ {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\schemaVar \term LocSet EQ ;
\assumes ( wellFormed ( h ) , select <[ LocSet ]> ( h , o , f ) = EQ ==> )
\find ( elementOf ( o2 , f2 , EQ ) ==> )
\add ( o2 = null | select <[ boolean ]> ( h , o2 , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 875 Offset :4onlyCreatedObjectsAreInLocSetsEQFinal {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\schemaVar \term LocSet EQ ;
\assumes ( wellFormed ( h ) , final <[ LocSet ]> ( o , f ) = EQ ==> )
\find ( elementOf ( o2 , f2 , EQ ) ==> )
\add ( o2 = null | select <[ boolean ]> ( h , o2 , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 892 Offset :4arrayLengthNotNegative {
\schemaVar \term Object o ;
\find ( length ( o ) )
\add ( length ( o ) >= 0 ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 912 Offset :4wellFormedStoreObject {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term deltaObject x ;
\find ( wellFormed ( store ( h , o , f , x ) ) )
\varcond \replacewith ( wellFormed ( h ) & ( x = null | select <[ boolean ]> ( h , x , java.lang.Object #$created ) = TRUE & instance <[ alpha ]> ( x ) = TRUE ) )
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 937 Offset :4wellFormedStoreArray {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term int idx ;
\schemaVar \term deltaObject x ;
\find ( wellFormed ( store ( h , o , arr ( idx ) , x ) ) )
\varcond \replacewith ( wellFormed ( h ) & ( x = null | select <[ boolean ]> ( h , x , java.lang.Object #$created ) = TRUE & arrayStoreValid ( o , x ) ) )
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 953 Offset :4wellFormedStoreLocSet {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet x ;
\find ( wellFormed ( store ( h , o , f , x ) ) )
\varcond \replacewith ( wellFormed ( h ) & createdInHeap ( x , h ) )
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 969 Offset :4wellFormedStorePrimitive {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term beta x ;
\find ( wellFormed ( store ( h , o , f , x ) ) )
\varcond \replacewith ( wellFormed ( h ) )
\heuristics (concrete )
};defined in: heapRules.key Line: 985 Offset :4wellFormedStorePrimitiveArray {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term int idx ;
\schemaVar \term beta x ;
\find ( wellFormed ( store ( h , o , arr ( idx ) , x ) ) )
\varcond \replacewith ( wellFormed ( h ) )
\heuristics (concrete )
};defined in: heapRules.key Line: 1004 Offset :4wellFormedCreate {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\find ( wellFormed ( create ( h , o ) ) )
\replacewith ( wellFormed ( h ) )
\heuristics (concrete )
};defined in: heapRules.key Line: 1024 Offset :4wellFormedMemsetArrayObject {
\schemaVar \term Heap h ;
\schemaVar \term Object ar ;
\schemaVar \term int lo , up ;
\schemaVar \term deltaObject x ;
\find ( wellFormed ( memset ( h , arrayRange ( ar , lo , up ) , x ) ) )
\varcond \replacewith ( wellFormed ( h ) & ( x = null | select <[ boolean ]> ( h , x , java.lang.Object #$created ) = TRUE & arrayStoreValid ( ar , x ) ) )
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 1048 Offset :4wellFormedMemsetArrayPrimitive {
\schemaVar \term Heap h ;
\schemaVar \term Object ar ;
\schemaVar \term int lo , up ;
\schemaVar \term beta x ;
\find ( wellFormed ( memset ( h , arrayRange ( ar , lo , up ) , x ) ) )
\varcond \replacewith ( wellFormed ( h ) )
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 1065 Offset :4wellFormedStoreObjectEQ {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term deltaObject x ;
\schemaVar \term Heap EQ ;
\assumes ( store ( h , o , f , x ) = EQ ==> )
\find ( wellFormed ( EQ ) )
\varcond \replacewith ( wellFormed ( h ) & ( x = null | select <[ boolean ]> ( h , x , java.lang.Object #$created ) = TRUE & instance <[ alpha ]> ( x ) = TRUE ) )
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 1149 Offset :4wellFormedStoreLocSetEQ {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet x ;
\schemaVar \term Heap EQ ;
\assumes ( store ( h , o , f , x ) = EQ ==> )
\find ( wellFormed ( EQ ) )
\replacewith ( wellFormed ( h ) & createdInHeap ( x , h ) )
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 1167 Offset :4wellFormedStorePrimitiveEQ {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term beta x ;
\schemaVar \term Heap EQ ;
\assumes ( store ( h , o , f , x ) = EQ ==> )
\find ( wellFormed ( EQ ) )
\varcond \replacewith ( wellFormed ( h ) )
\heuristics (concrete )
};defined in: heapRules.key Line: 1183 Offset :4wellFormedAnonEQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Heap EQ ;
\assumes ( anon ( h , s , h2 ) = EQ ==> )
\find ( wellFormed ( EQ ) )
\replacewith ( wellFormed ( h ) & wellFormed ( h2 ) )
\heuristics (concrete )
};defined in: heapRules.key Line: 1200 Offset :4onlyCreatedObjectsAreObserved {
\schemaVar \term Heap h ;
\schemaVar \term deltaObject obs ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( obs )
\varcond \add ( obs = null | select <[ boolean ]> ( h , obs , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 1271 Offset :4onlyCreatedObjectsAreObservedInLocSets {
\schemaVar \term Heap h ;
\schemaVar \term LocSet obs ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( elementOf ( o , f , obs ) ==> )
\varcond \add ( o = null | select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 1286 Offset :4onlyCreatedObjectsAreObservedInLocSetsEQ {
\schemaVar \term Heap h ;
\schemaVar \term LocSet obs , EQ ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( obs = EQ ==> )
\find ( elementOf ( o , f , EQ ) ==> )
\varcond \add ( o = null | select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 1301 Offset :4narrowSelectType {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( wellFormed ( h ) ==> )
\find ( select <[ beta ]> ( h , o , f ) )
\varcond \replacewith ( select <[ alpha ]> ( h , o , f ) )
\heuristics (simplify )
};defined in: heapRules.key Line: 1321 Offset :4narrowTypeFinal {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( final <[ beta ]> ( o , f ) )
\varcond \replacewith ( final <[ alpha ]> ( o , f ) )
\heuristics (simplify )
};defined in: heapRules.key Line: 1338 Offset :4narrowSelectArrayType {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term int idx ;
\assumes ( wellFormed ( h ) ==> o = null )
\find ( select <[ beta ]> ( h , o , arr ( idx ) ) )
\varcond \replacewith ( select <[ alpha ]> ( h , o , arr ( idx ) ) )
\heuristics (simplify )
};defined in: heapRules.key Line: 1353 Offset :4