proposition: Lemma v_in_range_data_at_: forall v p n sh, v_in_range v p (WORD_SIZE * n) -> data_at_ sh (tarray int_or_ptr_type n) p |-- EX m: Z, !!(0 < m <= Ptrofs.max_unsigned) && memory_block sh m v * TT.
proof: Proof. intros. destruct H as [o [? ?]]. rewrite data_at__memory_block. Intros. destruct H1 as [? [_ [? _]]]. destruct p; try contradiction. inv_int i. simpl offset_val in H0. rewrite ptrofs_add_repr in H0. assert (0 <= n)%Z by (unfold WORD_SIZE in *; rep_lia). rewrite sizeof_tarray_int_or_ptr by assumption. simpl in H2. rewrite Ptrofs.unsigned_repr in H2 by rep_lia. rewrite Z.max_r in H2 by assumption. fold WORD_SIZE in *. assert (WORD_SIZE * n = o + (WORD_SIZE * n - o))%Z by lia. remember (WORD_SIZE * n - o) as m. rewrite H5 in *. rewrite (memory_block_split sh b ofs o m) by lia. clear Heqm n H5 H3. assert (0 < m <= Ptrofs.max_unsigned) by rep_lia. rewrite <- H0. Exists m. 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