fact: Definition pq_make_spec := DECLARE _pq_make WITH size : Z PRE [tuint] PROP (4 <= 12 * size <= Int.max_unsigned) PARAMS (Vint (Int.repr size)) GLOBALS () SEP () POST [tptr t_pq] EX pq: val, EX h : heap, PROP (heap_size h = 0; heap_capacity h = size) LOCAL (temp ret_temp pq) SEP (valid_pq pq h).
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.env_binary_heap_pro