proposition: Lemma body_init: semax_body Vprog (@Gprog size inf _) f_init (@init_spec size _).
proof: Proof. start_function. assert (Int.max_signed < Int.max_unsigned) by now compute. forward_call (size * sizeof(tint)). 1: simpl; split; Lia.lia. Intro pq. forward. Exists pq. rewrite Z_div_mult by (simpl; lia). entailer!. rewrite Z.mul_comm. apply derives_refl. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.find_lemmas CertiGraph.priq.priq_arr_specs CertiGraph.priq.is_empty_lemmas CertiGraph.priq.priq_arr