proposition: Lemma single_outlier_rep_valid_int_or_ptr: forall p, single_outlier_rep p |-- !! (valid_int_or_ptr (GC_Pointer2val p)).
proof: Proof. intros. unfold single_outlier_rep. Intros sh. remember (GC_Pointer2val p) as pp. clear Heqpp. entailer!. destruct H0 as [? [_ [_ [? _]]]]. destruct pp; try contradiction. unfold align_compatible in H1. inv H1. inv H2. simpl in H3. fold WORD_SIZE in *. split. - simpl; apply (even_divided_odd_false WORD_SIZE); easy. - apply (four_divided_tenth_pl_false WORD_SIZE); [apply four_div_WORD_SIZE | easy]. 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