fact: Definition exch_spec := DECLARE _exch WITH j : Z, k : Z, arr: val, arr_contents: list heap_item, lookup : val, lookup_contents : list Z PRE [tuint, tuint, tptr t_item, tptr tuint] PROP (0 <= j < Zlength arr_contents; 0 <= k < Zlength arr_contents; Zlength arr_contents <= Int.max_unsigned; Zlength lookup_contents <= Int.max_unsigned) PARAMS (Vint (Int.repr j); Vint (Int.repr k); arr; lookup) GLOBALS () SEP (linked_heap_array arr_contents arr lookup_contents lookup) POST [tvoid] EX lookup_contents' : list Z, PROP (lookup_oob_eq (Zexchange arr_contents j k) lookup_contents lookup_contents') LOCAL () SEP (linked_heap_array (Zexchange arr_contents j k) arr lookup_contents' lookup).
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.env_binary_heap_pro