proposition: Lemma disj_memory_block: forall sh p1 n1 p2 n2, ~ pointer_range_overlap p1 n1 p2 n2 -> disjointed (memory_block sh n1 p1) (memory_block sh n2 p2).
proof: Proof. exact disj_memory_block. Qed.
imports: CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.alg_seplog CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.ramification_lemmas CertiGraph.veric_ext.seplog VST.veric.address_conflict VST.veric.SeparationLogic