fact: Definition sink_spec := DECLARE _sink WITH k : Z, arr: val, arr_contents: list heap_item, first_available : Z, lookup : val, lookup_contents : list Z PRE [tuint, tptr t_item, tuint, tptr tuint] PROP (0 <= k <= Zlength arr_contents; first_available = Zlength arr_contents; (k = Zlength arr_contents -> (2 * k) <= Int.max_unsigned); (k < Zlength arr_contents -> (2 * (first_available - 1) <= Int.max_unsigned)); weak_heap_ordered_top_down arr_contents k; Zlength lookup_contents <= Int.max_unsigned) PARAMS (Vint (Int.repr k); arr; Vint (Int.repr first_available); lookup) GLOBALS () SEP (linked_heap_array arr_contents arr lookup_contents lookup) POST [tvoid] EX arr_contents' : list heap_item, EX lookup_contents' : list Z, PROP (lookup_oob_eq arr_contents' lookup_contents lookup_contents'; heap_ordered arr_contents'; Permutation arr_contents arr_contents') LOCAL () SEP (linked_heap_array arr_contents' arr lookup_contents' lookup).
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.env_binary_heap_pro