KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Fri Aug 21 01:50:47 UTC 2026

Overview

wdHeapRules.key

Taclets

Enabled under choices: wdChecks:on

wd_Heap_ArrLength

wd_Heap_ArrLength { \find ( wd ( length ( o ) ) ) \varcond \replacewith ( wd ( o ) & o != null ) \heuristics (simplify ) };defined in: wdHeapRules.key Line: 15 Offset :4

wd_Heap_Create

wd_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 :4

wd_Heap_Reference_Created

wd_Heap_Reference_Created { \find ( wd ( select <[ alpha ]> ( h , o , java.lang.Object #$created ) ) ) \replacewith ( wd ( h ) & wd ( o ) & wellFormed ( h ) & o != null ) \heuristics (simplify ) };defined in: wdHeapRules.key Line: 40 Offset :4

wd_Heap_Reference

wd_Heap_Reference { \find ( wd ( select <[ alpha ]> ( h , o , f ) ) ) \varcond \replacewith ( wd ( h ) & wd ( o ) & wd ( f ) & wellFormed ( h ) & o != null & ( f = java.lang.Object #$created | select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE ) ) \heuristics (simplify ) };defined in: wdHeapRules.key Line: 51 Offset :4

wd_Heap_Reference_Static

wd_Heap_Reference_Static { \find ( wd ( select <[ alpha ]> ( h , o , f ) ) ) \varcond \replacewith ( wd ( h ) & wd ( o ) & wd ( f ) & wellFormed ( h ) & o = null ) \heuristics (simplify ) };defined in: wdHeapRules.key Line: 67 Offset :4

wd_Heap_Reference_Array

wd_Heap_Reference_Array { \find ( wd ( select <[ alpha ]> ( h , o , arr ( i ) ) ) ) \varcond \replacewith ( wd ( h ) & wd ( o ) & wd ( i ) & wellFormed ( h ) & o != null & select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE & leq ( 0 , i ) & lt ( i , length ( o ) ) ) \heuristics (simplify ) };defined in: wdHeapRules.key Line: 82 Offset :4

wd_Heap_Anon

wd_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 :4

wd_Heap_Memset

wd_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 :4

wd_Heap_Store

wd_Heap_Store { \find ( wd ( store ( h , o , f , a ) ) ) \replacewith ( wd ( h ) & wd ( o ) & wd ( f ) & wd ( a ) & wellFormed ( h ) & o != null & select <[ boolean ]> ( h , o , java.lang.Object #$created ) = TRUE ) \heuristics (simplify ) };defined in: wdHeapRules.key Line: 120 Offset :4

wd_Heap_Pred_WellFormed

wd_Heap_Pred_WellFormed { \find ( WD ( wellFormed ( h ) ) ) \replacewith ( wd ( h ) ) \heuristics (simplify ) };defined in: wdHeapRules.key Line: 132 Offset :4

wd_Heap_Pred_ArrStoreValid

wd_Heap_Pred_ArrStoreValid { \find ( WD ( arrayStoreValid ( a , b ) ) ) \replacewith ( wd ( a ) & wd ( b ) ) \heuristics (simplify ) };defined in: wdHeapRules.key Line: 143 Offset :4

wd_Heap_Pred_NonNull

wd_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