proposition: Lemma free_hitem: forall v, hitem_ v |-- data_at_ Tsh (tarray tint (sizeof (Tstruct _structItem noattr) / sizeof tint)) v.
proof: Proof. unfold hitem_. intro. saturate_local. sep_apply data_at__memory_block_cancel. rewrite <- memory_block_data_at_. apply derives_refl. destruct H as [? [? [? [? ?]]]]. split3; auto. split3; auto. hnf in H2 |- *. destruct v; auto. unfold t_item in H2. change (_ / _) with 3. apply align_compatible_rec_Tarray; intros. assert (i0 = 0 \/ i0 = 1 \/ i0 = 2) by lia. destruct H5 as [? | [? | ?]]; subst i0; [ eapply align_compatible_rec_Tstruct_inv with (i0 := _key) in H2 | eapply align_compatible_rec_Tstruct_inv with (i0 := _priority) in H2 | eapply align_compatible_rec_Tstruct_inv with (i0 := _data) in H2 ] ; try reflexivity; eapply align_compatible_rec_by_value; try reflexivity; eapply align_compatible_rec_by_value_inv in H2; try reflexivity; apply H2. Qed.
imports: RelationClasses VST.floyd.proofauto CertiGraph.lib.List_ext CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel