proposition: Lemma readable_writable_memory_block_FF: forall rsh wsh m1 m2 p, readable_share rsh -> writable_share wsh -> 0 < m1 <= Ptrofs.max_unsigned -> 0 < m2 <= Ptrofs.max_unsigned -> memory_block rsh m1 p * memory_block wsh m2 p |-- FF.
proof: Proof. intros. destruct (writable_readable_share_common _ _ H H0) as [sh [? [[shr ?] [shw ?]]]]. rewrite <- (memory_block_share_join _ _ _ _ _ H4). rewrite <- (memory_block_share_join _ _ _ _ _ H5). rewrite <- sepcon_assoc, (sepcon_comm (memory_block sh m1 p)), (sepcon_assoc (memory_block shr m1 p)). sep_apply (memory_block_conflict sh _ _ p H3 H1 H2). entailer!!. Qed.
imports: VST.veric.compcert_rmaps VST.msl.shares VST.msl.wand_frame VST.concurrency.conclib CertiGraph.lib.List_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.CertiGC.GCGraph CertiGraph.CertiGC.env_graph_gc CertiGraph.msl_ext.iter_sepcon Coq.Lists.List