wd_Heap_ArrLength {
\find ( wd ( length ( o )))
\varcond \replacewith ( wd ( o )& o != null )
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 15 Offset :4wd_Heap_Create {
\find ( wd ( create ( h , o )))
\replacewith ( wd ( h )& wd ( o )& wellFormed ( h )& o != null )
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 29 Offset :4wd_Heap_Reference_Created {
\find ( wd ( alpha :: select ( h , o , java.lang.Object :: )))
\replacewith ( wd ( h )& wd ( o )& wellFormed ( h )& o != null )
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 40 Offset :4wd_Heap_Reference {
\find ( wd ( alpha :: select ( h , o , f )))
\varcond \replacewith ( wd ( h )& wd ( o )& wd ( f )& wellFormed ( h )& o != null & ( f = java.lang.Object :: | boolean :: select ( h , o , java.lang.Object :: )= TRUE ))
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 51 Offset :4wd_Heap_Reference_Static {
\find ( wd ( alpha :: select ( h , o , f )))
\varcond \replacewith ( wd ( h )& wd ( o )& wd ( f )& wellFormed ( h )& o = null )
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 67 Offset :4wd_Heap_Reference_Array {
\find ( wd ( alpha :: select ( h , o , arr ( i ))))
\varcond \replacewith ( wd ( h )& wd ( o )& wd ( i )& wellFormed ( h )& o != null & boolean :: select ( h , o , java.lang.Object :: )= TRUE & leq ( 0 , i )& lt ( i , length ( o )))
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 82 Offset :4wd_Heap_Anon {
\find ( wd ( anon ( h , l , g )))
\replacewith ( wd ( h )& wd ( l )& wd ( g )& wellFormed ( h )& wellFormed ( g ))
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 98 Offset :4wd_Heap_Memset {
\find ( wd ( memset ( h , l , a )))
\replacewith ( wd ( h )& wd ( l )& wd ( a )& wellFormed ( h ))
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 109 Offset :4wd_Heap_Store {
\find ( wd ( store ( h , o , f , a )))
\replacewith ( wd ( h )& wd ( o )& wd ( f )& wd ( a )& wellFormed ( h )& o != null & boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 120 Offset :4wd_Heap_Pred_WellFormed {
\find ( WD ( wellFormed ( h )))
\replacewith ( wd ( h ))
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 132 Offset :4wd_Heap_Pred_ArrStoreValid {
\find ( WD ( arrayStoreValid ( a , b )))
\replacewith ( wd ( a )& wd ( b ))
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 143 Offset :4wd_Heap_Pred_NonNull {
\find ( WD ( nonNull ( h , o , i )))
\replacewith ( wd ( h )& wd ( o )& wd ( i ))
\heuristics (simplify )
};defined in: wdHeapRules.key Line: 153 Offset :4