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 & ! boolean :: select ( heapOld , o , java.lang.Object :: )= TRUE | any :: select ( heapNew , o , f )= any :: select ( 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 ( beta :: select ( store ( h , o , f , x ), o2 , f2 ))
\replacewith ( \if ( o = o2 & f = f2 & f != java.lang.Object :: )\then ( (beta ) x )\else ( beta :: select ( 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 ( beta :: select ( create ( h , o ), o2 , f ))
( permissions : off ) {
\replacewith ( \if ( o = o2 & o != null & f = java.lang.Object :: )\then ( (beta ) TRUE )\else ( beta :: select ( h , o2 , f )))}
;
( permissions : on ) {
\replacewith ( \if ( o = o2 & o != null )\then ( \if ( f = java.lang.Object :: )\then ( (beta ) TRUE )\else ( beta :: defaultValue ))\else ( beta :: select ( 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 ( beta :: select ( anon ( h , s , h2 ), o , f ))
\replacewith ( \if ( elementOf ( o , f , s )& f != java.lang.Object :: | elementOf ( o , f , freshLocs ( h )))\then ( beta :: select ( h2 , o , f ))\else ( beta :: select ( 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 ( beta :: select ( memset ( h , s , x ), o , f ))
\replacewith ( \if ( elementOf ( o , f , s )& f != java.lang.Object :: )\then ( (beta ) x )\else ( beta :: select ( h , o , f )))
\heuristics (semantics_blasting )
};defined in: heapRules.key Line: 89 Offset :4nullCreated {
\schemaVar \variables Heap h ;
\add ( ( \forall h ; boolean :: select ( h , null , java.lang.Object :: )= TRUE )| ( \forall h ; boolean :: select ( h , null , java.lang.Object :: )= FALSE )==> )
};defined in: heapRules.key Line: 112 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 ( beta :: select ( EQ , o2 , f2 ))
\sameUpdateLevel
\replacewith ( \if ( o = o2 & f = f2 & f != java.lang.Object :: )\then ( (beta ) x )\else ( beta :: select ( 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 ( beta :: select ( EQ , o2 , f ))
\sameUpdateLevel
( permissions : off ) {
\replacewith ( \if ( o = o2 & o != null & f = java.lang.Object :: )\then ( (beta ) TRUE )\else ( beta :: select ( h , o2 , f )))}
;
( permissions : on ) {
\replacewith ( \if ( o = o2 & o != null )\then ( \if ( f = java.lang.Object :: )\then ( (beta ) TRUE )\else ( beta :: defaultValue ))\else ( beta :: select ( h , o2 , f )))}
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 142 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 ( beta :: select ( EQ , o , f ))
\sameUpdateLevel
\replacewith ( \if ( elementOf ( o , f , s )& f != java.lang.Object :: | elementOf ( o , f , freshLocs ( h )))\then ( beta :: select ( h2 , o , f ))\else ( beta :: select ( h , o , f )))
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 166 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 ( beta :: select ( EQ , o , f ))
\sameUpdateLevel
\replacewith ( \if ( elementOf ( o , f , s )& f != java.lang.Object :: )\then ( (beta ) x )\else ( beta :: select ( h , o , f )))
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 185 Offset :4pullOutSelect {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \skolemTerm beta selectSK ;
\find ( beta :: select ( h , o , f ))
\sameUpdateLevel
\replacewith ( selectSK << selectSK >> ) \add ( beta :: select ( h , o , f )= selectSK << selectSK >> ==> )
\heuristics (pull_out_select )
};defined in: heapRules.key Line: 334 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 ( beta :: select ( store ( h , o , f , x ), o2 , f2 )= sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( o = o2 & f = f2 & f != java.lang.Object :: )\then ( (beta ) x )\else ( beta :: select ( h , o2 , f2 ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( store ( h , o , f , x ), o2 , f2 ))
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 348 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 ( beta :: select ( EQ , o2 , f2 )= sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( o = o2 & f = f2 & f != java.lang.Object :: )\then ( (beta ) x )\else ( beta :: select ( h , o2 , f2 ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( EQ , o2 , f2 ))
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 375 Offset :4simplifySelectOfCreate {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f ;
\schemaVar \term beta sk ;
\find ( beta :: select ( create ( h , o ), o2 , f )= sk ==> )
\inSequentState
\inSequentState
( permissions : off ) {
\replacewith ( \if ( o = o2 & o != null & f = java.lang.Object :: )\then ( (beta ) TRUE )\else ( beta :: select ( h , o2 , f ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( 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 :: )\then ( (beta ) TRUE )\else ( beta :: defaultValue ))\else ( beta :: select ( h , o2 , f ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( create ( h , o ), o2 , f ))
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)}
\heuristics (simplify_select )
};defined in: heapRules.key Line: 403 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 ( beta :: select ( EQ , o2 , f )= sk ==> )
\inSequentState
\inSequentState
( permissions : off ) {
\replacewith ( \if ( o = o2 & o != null & f = java.lang.Object :: )\then ( (beta ) TRUE )\else ( beta :: select ( h , o2 , f ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( EQ , o2 , f ))
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)}
;
( permissions : on ) {
\replacewith ( \if ( o = o2 & o != null )\then ( \if ( f = java.lang.Object :: )\then ( (beta ) TRUE )\else ( beta :: defaultValue ))\else ( beta :: select ( h , o2 , f ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( EQ , o2 , f ))
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)}
\heuristics (simplify_select )
};defined in: heapRules.key Line: 444 Offset :4simplifySelectOfAnon {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term beta sk ;
\find ( beta :: select ( anon ( h , s , h2 ), o , f )= sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( elementOf ( o , f , s )& f != java.lang.Object :: | elementOf ( o , f , freshLocs ( h )))\then ( beta :: select ( h2 , o , f ))\else ( beta :: select ( h , o , f ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( anon ( h , s , h2 ), o , f ))
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 486 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 ( beta :: select ( EQ , o , f )= sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( elementOf ( o , f , s )& f != java.lang.Object :: | elementOf ( o , f , freshLocs ( h )))\then ( beta :: select ( h2 , o , f ))\else ( beta :: select ( h , o , f ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( EQ , o , f ))
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 514 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 ( beta :: select ( memset ( h , s , x ), o , f )= sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( elementOf ( o , f , s )& f != java.lang.Object :: )\then ( x )\else ( beta :: select ( h , o , f ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( memset ( h , s , x ), o , f ))
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 543 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 ( beta :: select ( EQ , o , f )= sk ==> )
\inSequentState
\inSequentState
\replacewith ( \if ( elementOf ( o , f , s )& f != java.lang.Object :: )\then ( x )\else ( beta :: select ( h , o , f ))= sk ==> ) \addrules ( replaceKnownSelect {
\find ( beta :: select ( EQ , o , f ))
\inSequentState
\inSequentState
\replacewith ( sk )
\heuristics (concrete )
};)
\heuristics (simplify_select )
};defined in: heapRules.key Line: 571 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: 604 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: 619 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: 634 Offset :4dismissNonSelectedField {
\schemaVar \term Heap h ;
\schemaVar \term Object o , u ;
\schemaVar \term Field f1 , f2 ;
\schemaVar \term any x ;
\find ( alpha :: select ( store ( h , o , f1 , x ), u , f2 ))
\varcond \replacewith ( alpha :: select ( h , u , f2 ))
\heuristics (simplify )
};defined in: heapRules.key Line: 657 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 ( alpha :: select ( EQ , u , f2 ))
\sameUpdateLevel
\varcond \replacewith ( alpha :: select ( h , u , f2 ))
\heuristics (simplify )
};defined in: heapRules.key Line: 672 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: 688 Offset :4memsetEmpty {
\schemaVar \term Heap h ;
\schemaVar \term any x ;
\find ( memset ( h , empty , x ))
\replacewith ( h )
\heuristics (concrete )
};defined in: heapRules.key Line: 702 Offset :4selectCreatedOfAnon {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\find ( boolean :: select ( anon ( h , s , h2 ), o , java.lang.Object :: ))
\replacewith ( \if ( boolean :: select ( h , o , java.lang.Object :: )= TRUE )\then ( TRUE )\else ( boolean :: select ( h2 , o , java.lang.Object :: )))
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 735 Offset :4selectCreatedOfAnonAsFormula {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\find ( boolean :: select ( anon ( h , s , h2 ), o , java.lang.Object :: )= TRUE )
\replacewith ( boolean :: select ( h , o , java.lang.Object :: )= TRUE | boolean :: select ( h2 , o , java.lang.Object :: )= TRUE )
\heuristics (simplify_ENLARGING )
};defined in: heapRules.key Line: 750 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 ( boolean :: select ( EQ , o , java.lang.Object :: ))
\sameUpdateLevel
\replacewith ( \if ( boolean :: select ( h , o , java.lang.Object :: )= TRUE )\then ( TRUE )\else ( boolean :: select ( h2 , o , java.lang.Object :: )))
\heuristics (simplify_heap_high_costs )
};defined in: heapRules.key Line: 764 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 ( boolean :: select ( EQ , o , java.lang.Object :: )= TRUE )
\sameUpdateLevel
\replacewith ( boolean :: select ( h , o , java.lang.Object :: )= TRUE | boolean :: select ( h2 , o , java.lang.Object :: )= TRUE )
\heuristics (simplify_ENLARGING )
};defined in: heapRules.key Line: 782 Offset :4equalityToSelect {
\schemaVar \term Heap h , h2 ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\find ( h = h2 )
\varcond \replacewith ( \forall ov ; \forall fv ; ( any :: select ( h , ov , fv )= any :: select ( h2 , ov , fv )))
\heuristics (semantics_blasting )
};defined in: heapRules.key Line: 798 Offset :4onlyCreatedObjectsAreReferenced {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( wellFormed ( h )==> )
\find ( deltaObject :: select ( h , o , f ))
\sameUpdateLevel
\add ( deltaObject :: select ( h , o , f )= null | boolean :: select ( h , deltaObject :: select ( h , o , f ), java.lang.Object :: )= TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 816 Offset :4onlyCreatedObjectsAreInLocSets {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\assumes ( wellFormed ( h )==> )
\find ( elementOf ( o2 , f2 , LocSet :: select ( h , o , f ))==> )
\add ( o2 = null | boolean :: select ( h , o2 , java.lang.Object :: )= TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 833 Offset :4onlyCreatedObjectsAreInLocSetsEQ {
\schemaVar \term Heap h ;
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\schemaVar \term LocSet EQ ;
\assumes ( wellFormed ( h ), LocSet :: select ( h , o , f )= EQ ==> )
\find ( elementOf ( o2 , f2 , EQ )==> )
\add ( o2 = null | boolean :: select ( h , o2 , java.lang.Object :: )= TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 849 Offset :4arrayLengthNotNegative {
\schemaVar \term Object o ;
\find ( length ( o ))
\sameUpdateLevel
\add ( length ( o )>= 0 ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 866 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 | boolean :: select ( h , x , java.lang.Object :: )= TRUE & alpha :: instance ( x )= TRUE ))
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 893 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 | boolean :: select ( h , x , java.lang.Object :: )= TRUE & arrayStoreValid ( o , x )))
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 909 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: 925 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: 941 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: 960 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: 980 Offset :4wellFormedAnon {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\find ( wellFormed ( anon ( h , s , h2 )))
\replacewith ( wellFormed ( h )& wellFormed ( h2 ))
\heuristics (concrete )
};defined in: heapRules.key Line: 992 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 | boolean :: select ( h , x , java.lang.Object :: )= TRUE & arrayStoreValid ( ar , x )))
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 1004 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: 1021 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 ))
\sameUpdateLevel
\varcond \replacewith ( wellFormed ( h )& ( x = null | boolean :: select ( h , x , java.lang.Object :: )= TRUE & alpha :: instance ( x )= TRUE ))
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 1105 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 ))
\sameUpdateLevel
\replacewith ( wellFormed ( h )& createdInHeap ( x , h ))
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 1124 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 ))
\sameUpdateLevel
\varcond \replacewith ( wellFormed ( h ))
\heuristics (concrete )
};defined in: heapRules.key Line: 1141 Offset :4wellFormedAnonEQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Heap EQ ;
\assumes ( anon ( h , s , h2 )= EQ ==> )
\find ( wellFormed ( EQ ))
\sameUpdateLevel
\replacewith ( wellFormed ( h )& wellFormed ( h2 ))
\heuristics (concrete )
};defined in: heapRules.key Line: 1159 Offset :4onlyCreatedObjectsAreObserved {
\schemaVar \term Heap h ;
\schemaVar \term deltaObject obs ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( obs )
\sameUpdateLevel
\varcond \add ( obs = null | boolean :: select ( h , obs , java.lang.Object :: )= TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 1234 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 | boolean :: select ( h , o , java.lang.Object :: )= TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 1250 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 | boolean :: select ( h , o , java.lang.Object :: )= TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 1265 Offset :4narrowSelectType {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( wellFormed ( h )==> )
\find ( beta :: select ( h , o , f ))
\varcond \replacewith ( alpha :: select ( h , o , f ))
\heuristics (simplify )
};defined in: heapRules.key Line: 1285 Offset :4narrowSelectArrayType {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term int idx ;
\assumes ( wellFormed ( h )==> o = null )
\find ( beta :: select ( h , o , arr ( idx )))
\sameUpdateLevel
\varcond \replacewith ( alpha :: select ( h , o , arr ( idx )))
\heuristics (simplify )
};defined in: heapRules.key Line: 1302 Offset :4castTrueImpliesOriginalTrue {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( boolean :: select ( h , o , f )= TRUE ==> )
\find ( ==> any :: select ( h , o , f )= TRUE )
\replacewith ( ==> true )
\heuristics (concrete )
};defined in: heapRules.key Line: 1320 Offset :4arrayLengthIsAShort {
\schemaVar \term Object o ;
\find ( length ( o ))
\sameUpdateLevel
\add ( inShort ( length ( o ))==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 1336 Offset :4arrayLengthIsAnInt {
\schemaVar \term Object o ;
\find ( length ( o ))
\sameUpdateLevel
\add ( inInt ( length ( o ))==> )
\heuristics (inReachableStateImplication )
};defined in: heapRules.key Line: 1350 Offset :4observerDependencyEQ {
\schemaVar \term any t1 ;
\schemaVar \term any t2 ;
\find ( t1 = t2 )
\inSequentState
\inSequentState
\varcond \replacewith ( true );
\add ( ==> #ObserverEquality ( t1 , t2 ))
};defined in: heapRules.key Line: 1364 Offset :4observerDependencyEquiv {
\schemaVar \formula t1 ;
\schemaVar \formula t2 ;
\find ( t1 <-> t2 )
\inSequentState
\inSequentState
\varcond \replacewith ( true );
\add ( ==> #ObserverEquality ( t1 , t2 ))
\displayname "observerDependencyEQ"
};defined in: heapRules.key Line: 1376 Offset :4observerDependency {
\schemaVar \term any termWithLargeHeap ;
\schemaVar \term any termWithSmallHeap ;
\find ( termWithLargeHeap )
\inSequentState
\inSequentState
\varcond \replacewith ( termWithSmallHeap );
\add ( ==> #ObserverEquality ( termWithLargeHeap , termWithSmallHeap ))
};defined in: heapRules.key Line: 1389 Offset :4observerDependencyFormula {
\schemaVar \formula termWithLargeHeap ;
\schemaVar \formula termWithSmallHeap ;
\find ( termWithLargeHeap )
\inSequentState
\inSequentState
\varcond \replacewith ( termWithSmallHeap );
\add ( ==> #ObserverEquality ( termWithLargeHeap , termWithSmallHeap ))
\displayname "observerDependency"
};defined in: heapRules.key Line: 1401 Offset :4nonNull {
\schemaVar \term Object o ;
\schemaVar \term Heap heapSV ;
\schemaVar \term int depth ;
\schemaVar \variables int i ;
\find ( nonNull ( heapSV , o , depth ))
\varcond \replacewith ( ( o != null & ( depth > 0 -> \forall i ; ( 0 <= i & i < length ( o )-> nonNull ( heapSV , Object :: select ( heapSV , o , arr ( i )), depth - 1 )))))
\heuristics (simplify_enlarging )
};defined in: heapRules.key Line: 1414 Offset :4nullIsNotNonNull {
\schemaVar \term Object o ;
\schemaVar \term Heap heapSV ;
\schemaVar \term int depth ;
\find ( nonNull ( heapSV , null , depth ))
\replacewith ( false )
\heuristics (concrete )
};defined in: heapRules.key Line: 1431 Offset :4nonNullZero {
\schemaVar \term Object o ;
\schemaVar \term Heap heapSV ;
\find ( nonNull ( heapSV , o , 0 ))
\replacewith ( o != null )
\heuristics (concrete )
};defined in: heapRules.key Line: 1440 Offset :4