diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-15 16:24:13 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-15 16:24:13 +0000 |
| commit | f774d5f2d604f747e72e2d3bb56cc3f90090e2dd (patch) | |
| tree | 05a5bcfc207c67f58575fa7b61787c0c9dbe8215 /cfrontend/Initializersproof.v | |
| parent | f1ceca440c0322001abe6c5de79bd4bc309fc002 (diff) | |
Pointers one past
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Initializersproof.v')
| -rw-r--r-- | cfrontend/Initializersproof.v | 15 |
1 files changed, 12 insertions, 3 deletions
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: |