accDefinition {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term deltaObject o2 ;
\schemaVar \variables Field fv ;
\find ( acc ( h , s , o , o2 ) )
\varcond \replacewith ( o != null & o2 != null & \exists fv ; ( elementOf ( o , fv , s ) & select <[ deltaObject ]> ( h , o , fv ) = o2 ) )
\heuristics (simplify )
};defined in: reachRules.key Line: 11 Offset :4reachDefinition {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\find ( reach ( h , s , o , o2 , n ) )
\varcond \replacewith ( n >= 0 & o != null & o2 != null & ( n = 0 & o = o2 | \exists ov ; ( reach ( h , s , o , ov , n - 1 ) & acc ( h , s , ov , o2 ) ) ) )
};defined in: reachRules.key Line: 30 Offset :4reachZero {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\find ( reach ( h , s , o , o2 , 0 ) )
\replacewith ( o != null & o = o2 )
\heuristics (simplify )
};defined in: reachRules.key Line: 57 Offset :4reachOne {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\find ( reach ( h , s , o , o2 , 1 ) )
\replacewith ( acc ( h , s , o , o2 ) )
\heuristics (simplify )
};defined in: reachRules.key Line: 69 Offset :4reachNull {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term int n ;
\find ( reach ( h , s , o , null , n ) )
\replacewith ( false)
\heuristics (simplify )
};defined in: reachRules.key Line: 81 Offset :4reachNull2 {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o2 ;
\schemaVar \term int n ;
\find ( reach ( h , s , null , o2 , n ) )
\replacewith ( false)
\heuristics (simplify )
};defined in: reachRules.key Line: 94 Offset :4reachAddOne {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\find ( reach ( h , s , o , o2 , 1 + n ) )
\varcond \replacewith ( n >= - 1 & o != null & o2 != null & ( n = - 1 & o = o2 | \exists ov ; ( reach ( h , s , o , ov , n ) & acc ( h , s , ov , o2 ) ) ) )
\heuristics (simplify )
};defined in: reachRules.key Line: 107 Offset :4reachAddOne2 {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\find ( reach ( h , s , o , o2 , n + 1 ) )
\varcond \replacewith ( n >= - 1 & o != null & o2 != null & ( n = - 1 & o = o2 | \exists ov ; ( reach ( h , s , o , ov , n ) & acc ( h , s , ov , o2 ) ) ) )
\heuristics (simplify )
};defined in: reachRules.key Line: 131 Offset :4reachUniquePathSameSteps {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\schemaVar \term Field f ;
\assumes ( reach ( h , allObjects ( f ) , o , o2 , n ) ==> )
\find ( reach ( h , allObjects ( f ) , o , o3 , n ) ==> )
\varcond \add ( o2 = o3 ==> )
\heuristics (inReachableStateImplication )
};defined in: reachRules.key Line: 155 Offset :4reachEndOfUniquePath {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n , n2 ;
\schemaVar \term Field f ;
\assumes ( reach ( h , allObjects ( f ) , o , o2 , n ) , select <[ alpha ]> ( h , o2 , f ) = null , select <[ alpha ]> ( h , o3 , f ) = null ==> )
\find ( reach ( h , allObjects ( f ) , o , o3 , n2 ) ==> )
\varcond \add ( o2 = o3 & n = n2 ==> )
\heuristics (inReachableStateImplication )
};defined in: reachRules.key Line: 171 Offset :4reachEndOfUniquePath2 {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n , n2 ;
\schemaVar \term Field f ;
\assumes ( reach ( h , allObjects ( f ) , o , o2 , n ) , select <[ alpha ]> ( h , o2 , f ) = null ==> )
\find ( reach ( h , allObjects ( f ) , o , o3 , n2 ) ==> )
\varcond \add ( n2 < n | ( o2 = o3 & n = n2 ) ==> )
\heuristics (inReachableStateImplication )
};defined in: reachRules.key Line: 189 Offset :4reachDependenciesStoreSimple {
\schemaVar \term Heap h ;
\schemaVar \term Field f , f2 ;
\schemaVar \term any x ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\find ( reach ( store ( h , o3 , f2 , x ) , allObjects ( f ) , o , o2 , n ) )
\varcond \replacewith ( reach ( h , allObjects ( f ) , o , o2 , n ) )
\heuristics (simplify )
};defined in: reachRules.key Line: 206 Offset :4reachDependenciesStoreSimpleEQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term Field f , f2 ;
\schemaVar \term any x ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\assumes ( store ( h , o3 , f2 , x ) = h2 ==> )
\find ( reach ( h2 , allObjects ( f ) , o , o2 , n ) )
\varcond \replacewith ( reach ( h , allObjects ( f ) , o , o2 , n ) )
\heuristics (simplify )
};defined in: reachRules.key Line: 221 Offset :4reachDoesNotDependOnCreatedness {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\find ( reach ( create ( h , o3 ) , s , o , o2 , n ) )
\replacewith ( reach ( h , s , o , o2 , n ) )
\heuristics (simplify )
};defined in: reachRules.key Line: 237 Offset :4reachDependenciesStore {
\schemaVar \term Heap h ;
\schemaVar \term Field f ;
\schemaVar \term any x ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\schemaVar \variables int nv ;
\find ( reach ( store ( h , o3 , f , x ) , s , o , o2 , n ) )
\varcond "Dependencies changed" : \add ( ==> ! ( \exists nv ; ( nv < n & reach ( h , s , o , o3 , nv ) ) & elementOf ( o3 , f , s ) ) ) ;
"Dependencies unchanged" : \replacewith ( reach ( h , s , o , o2 , n ) ) \add ( ! ( \exists nv ; ( nv < n & reach ( h , s , o , o3 , nv ) ) & elementOf ( o3 , f , s ) ) ==> )
};defined in: reachRules.key Line: 249 Offset :4reachDependenciesStoreEQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term Field f ;
\schemaVar \term any x ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 , o3 ;
\schemaVar \term int n ;
\schemaVar \variables int nv ;
\assumes ( store ( h , o3 , f , x ) = h2 ==> )
\find ( reach ( h2 , s , o , o2 , n ) )
\varcond "Dependencies changed" : \add ( ==> ! ( \exists nv ; ( nv < n & reach ( h , s , o , o3 , nv ) ) & elementOf ( o3 , f , s ) ) ) ;
"Dependencies unchanged" : \replacewith ( reach ( h , s , o , o2 , n ) ) \add ( ! ( \exists nv ; ( nv < n & reach ( h , s , o , o3 , nv ) ) & elementOf ( o3 , f , s ) ) ==> )
};defined in: reachRules.key Line: 277 Offset :4reachDependenciesAnon {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\schemaVar \variables int nv ;
\find ( reach ( anon ( h , s2 , h2 ) , s , o , o2 , n ) )
\varcond "Dependencies changed" : \add ( ==> \forall ov ; \forall fv ; ! ( elementOf ( ov , fv , s2 ) & \exists nv ; ( nv < n & reach ( h , s , o , ov , nv ) ) & elementOf ( ov , fv , s ) ) ) ;
"Dependencies unchanged" : \replacewith ( reach ( h , s , o , o2 , n ) ) \add ( \forall ov ; \forall fv ; ! ( elementOf ( ov , fv , s2 ) & \exists nv ; ( nv < n & reach ( h , s , o , ov , nv ) ) & elementOf ( ov , fv , s ) ) ==> )
};defined in: reachRules.key Line: 306 Offset :4reachDependenciesAnonCoarse {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\schemaVar \variables int nv ;
\find ( reach ( anon ( h , s2 , h2 ) , s , o , o2 , n ) )
\varcond "Dependencies changed" : \add ( ==> \forall ov ; \forall fv ; ! ( elementOf ( ov , fv , s2 ) & \exists nv ; ( reach ( h , s , o , ov , nv ) ) & elementOf ( ov , fv , s ) ) ) ;
"Dependencies unchanged" : \replacewith ( reach ( h , s , o , o2 , n ) ) \add ( \forall ov ; \forall fv ; ! ( elementOf ( ov , fv , s2 ) & \exists nv ; ( reach ( h , s , o , ov , nv ) ) & elementOf ( ov , fv , s ) ) ==> )
};defined in: reachRules.key Line: 347 Offset :4only_created_objects_are_reachable {
\schemaVar \term Heap h ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\assumes ( wellFormed ( h ) ==> o = null )
\find ( reach ( h , s , o , o2 , n ) ==> )
\add ( ! select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE | select <[ boolean ]> ( h , o2 , java.lang.Object #$created ) = TRUE ==> )
\heuristics (inReachableStateImplication )
};defined in: reachRules.key Line: 388 Offset :4reach_does_not_depend_on_fresh_locs {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\assumes ( ==> o = null )
\find ( reach ( anon ( h , empty , h2 ) , s , o , o2 , n ) )
\replacewith ( reach ( h , s , o , o2 , n ) ) ;
\add ( ==> wellFormed ( h ) & select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE )
\heuristics (simplify )
};defined in: reachRules.key Line: 401 Offset :4reach_does_not_depend_on_fresh_locs_EQ {
\schemaVar \term Heap h , h2 ;
\schemaVar \term LocSet s ;
\schemaVar \term Object o , o2 ;
\schemaVar \term int n ;
\schemaVar \term Heap EQ ;
\assumes ( anon ( h , empty , h2 ) = EQ ==> o = null )
\find ( reach ( EQ , s , o , o2 , n ) )
\replacewith ( reach ( h , s , o , o2 , n ) ) ;
\add ( ==> wellFormed ( h ) & select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE )
\heuristics (simplify )
};defined in: reachRules.key Line: 416 Offset :4