proposition: Lemma single_outlier_rep_valid_pointer: forall p, single_outlier_rep p |-- valid_pointer (GC_Pointer2val p) * TT.
proof: Proof. intros. unfold single_outlier_rep. Intros sh. remember (GC_Pointer2val p) as pp. sep_apply (data_at__memory_block_cancel sh (tptr tvoid) pp). simpl sizeof. fold WORD_SIZE. sep_apply (memory_block_valid_ptr sh WORD_SIZE pp); [apply readable_nonidentity; assumption | apply derives_refl]. 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