From 72c5d592af9c9c0b417becc6abe5c2364d81639a Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 30 May 2008 14:28:57 +0000 Subject: 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 --- common/Mem.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'common/Mem.v') diff --git a/common/Mem.v b/common/Mem.v index d369b808..35d93ed7 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: -- cgit