proposition: Lemma data_at_conflict: forall sh t1 t2 p1 p2 v1 v2, sepalg.nonunit sh -> pointer_range_overlap p1 (sizeof t1) p2 (sizeof t2) -> data_at sh t1 v1 p1 * data_at sh t2 v2 p2 |-- FF.
proof: Proof. intros. eapply derives_trans; [apply sepcon_derives; apply data_at_memory_block |]. apply mapsto_memory_block.memory_block_overlap; auto. Qed.
imports: VST.floyd.base VST.floyd.client_lemmas VST.floyd.assert_lemmas VST.floyd.type_induction VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.reptype_lemmas VST.floyd.field_at CertiGraph.veric_ext.seplog CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.MapstoSL