proposition: Lemma pointer_range_overlap_sizeof: forall {cs: composite_env} sh p1 p2 t1 t2, pointer_range_overlap p1 (sizeof t1) p2 (sizeof t2) -> pointer_range_overlap p1 (BV_sizeof t1) p2 (BV_sizeof t2) \/ (EX v: val, mapsto sh t1 p1 v |-- FF) \/ (EX v: val, mapsto sh t2 p2 v |-- FF).
proof: Proof. pose proof (@exp_FF mpred val _) as EXP_FF. change (@seplog.exp _ _ val) with (@exp _ _ val) in EXP_FF. change seplog.FF with FF in EXP_FF. intros. unfold BV_sizeof. unfold mapsto. destruct (access_mode t1) eqn:?H; try solve [right; left; rewrite EXP_FF; auto]. destruct (access_mode t2) eqn:?H; try solve [right; right; rewrite EXP_FF; auto]. left. erewrite !size_chunk_sizeof in H by eauto. auto. Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize VST.veric.base VST.veric.rmaps VST.veric.rmaps_lemmas VST.veric.compcert_rmaps VST.veric.slice VST.veric.res_predicates VST.veric.tycontext VST.veric.expr VST.veric.address_conflict VST.veric.seplog VST.veric.mapsto_memory_block VST.msl.msl_standard VST.msl.alg_seplog CertiGraph.msl_ext.alg_seplog CertiGraph.veric_ext.res_predicates