fact: Definition pq_size_spec := DECLARE _pq_size WITH pq : val, h : heap PRE [tptr t_pq] PROP () PARAMS (pq) GLOBALS () SEP (valid_pq pq h) POST [tuint] PROP () LOCAL (temp ret_temp (Vint (Int.repr (heap_size h)))) 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