diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 14:28:57 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 14:28:57 +0000 |
| commit | 72c5d592af9c9c0b417becc6abe5c2364d81639a (patch) | |
| tree | 96b5b896605b31ab6ddab385b33fda87a8a40d8a /common | |
| parent | f4b41226d60ca57c5981b0a46e0a495152b5301f (diff) | |
Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs vers des blocs differents!
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common')
| -rw-r--r-- | common/Mem.v | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/common/Mem.v b/common/Mem.v index d369b80..35d93ed 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -1870,6 +1870,30 @@ Proof. eapply valid_pointer_inj; eauto. Qed. +Lemma different_pointers_inject: + forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, + mem_inject f m m' -> + b1 <> b2 -> + valid_pointer m b1 (Int.signed ofs1) = true -> + valid_pointer m b2 (Int.signed ofs2) = true -> + f b1 = Some (b1', delta1) -> + f b2 = Some (b2', delta2) -> + b1' <> b2' \/ + Int.signed (Int.add ofs1 (Int.repr delta1)) <> + Int.signed (Int.add ofs2 (Int.repr delta2)). +Proof. + intros. + rewrite valid_pointer_valid_access in H1. + rewrite valid_pointer_valid_access in H2. + rewrite (address_inject _ _ _ _ _ _ _ _ H H1 H3). + rewrite (address_inject _ _ _ _ _ _ _ _ H H2 H4). + inv H1. simpl in H7. inv H2. simpl in H9. + exploit (mi_no_overlap _ _ _ H); eauto. + intros [A | [A | [A | [A | A]]]]. + auto. omegaContradiction. omegaContradiction. + right. omega. right. omega. +Qed. + (** Relation between injections and loads. *) Lemma load_inject: |