From f774d5f2d604f747e72e2d3bb56cc3f90090e2dd Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Feb 2013 16:24:13 +0000 Subject: Pointers one past git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Initializersproof.v | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'cfrontend/Initializersproof.v') diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index ca9c5b0..b64c309 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -380,6 +380,13 @@ Proof. eelim Mem.perm_empty; eauto. Qed. +Lemma mem_empty_not_weak_valid_pointer: + forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false. +Proof. + intros. unfold Mem.weak_valid_pointer. + now rewrite !mem_empty_not_valid_pointer. +Qed. + Lemma sem_cmp_match: forall c v1 ty1 v2 ty2 m v v1' v2' v', sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v -> @@ -391,10 +398,12 @@ Opaque zeq. intros. unfold sem_cmp in *. destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval. destruct (Int.eq n Int.zero); try discriminate. - unfold sem_cmp_mismatch in *. destruct c; inv H3; inv H2; constructor. + unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor. destruct (Int.eq n Int.zero); try discriminate. - unfold sem_cmp_mismatch in *. destruct c; inv H2; inv H1; constructor. - rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. discriminate. + unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor. + rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. + rewrite (mem_empty_not_weak_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. simpl in H4. + destruct (zeq (Z.pos id) (Z.pos id0)); discriminate. Qed. Lemma sem_binary_match: -- cgit v1.2.3