fact: Definition freePQ_spec {CS: compspecs} := DECLARE _freePQ WITH sh: share, p: pointer_val, n: Z, contents: list Z PRE [tptr tvoid] PROP () PARAMS (pointer_val_val p) GLOBALS () SEP (data_at sh (tarray tint n) (map Vint (map Int.repr contents)) (pointer_val_val p) * free_tok (pointer_val_val p) (sizeof tint * n)) POST [tvoid] PROP () LOCAL () SEP (emp).
imports: VST.floyd.proofauto CertiGraph.lib.find_lemmas CertiGraph.priq.is_empty_lemmas CertiGraph.priq.priq_arr