proposition: Lemma single_outlier_rep_memory_block_FF: forall gp p n wsh, writable_share wsh -> v_in_range (GC_Pointer2val gp) p (WORD_SIZE * n) -> single_outlier_rep gp * data_at_ wsh (tarray int_or_ptr_type n) p |-- FF.
proof: Proof. intros. unfold single_outlier_rep. Intros rsh. remember (GC_Pointer2val gp) as ggp. clear gp Heqggp. rename ggp into gp. sep_apply (v_in_range_data_at_ _ _ _ wsh H0). Intros m. sep_apply (data_at__memory_block_cancel rsh (tptr tvoid) gp). simpl sizeof. rewrite <- sepcon_assoc. fold WORD_SIZE. sep_apply (readable_writable_memory_block_FF _ _ WORD_SIZE m gp H1 H); auto; [unfold WORD_SIZE; rep_lia | 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