Pointers one past

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 26 insertions, 15 deletions

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9bbf040..a61808a 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1573,26 +1573,37 @@ Proof.
     apply val_inject_val_of_optbool.
     apply val_inject_val_of_optbool.
 Opaque Int.add.
-    unfold Val.cmpu. simpl. 
-    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; simpl; auto.
-    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; simpl; auto.
-    exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb. econstructor; eauto. 
-    intros V1. rewrite V1.
-    exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. 
-    intros V2. rewrite V2. simpl.
-    destruct (zeq b1 b0).
+    unfold Val.cmpu. simpl.
+    destruct (zeq b1 b0); subst.
     (* same blocks *)
-    subst b1. rewrite H in H0; inv H0. rewrite zeq_true. 
-    rewrite Int.translate_cmpu. apply val_inject_val_of_optbool.
-    eapply Mem.valid_pointer_inject_no_overflow; eauto.
-    eapply Mem.valid_pointer_inject_no_overflow; eauto.
+    rewrite H0 in H. inv H. rewrite zeq_true.
+    fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)).
+    fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)).
+    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs0 (Int.repr delta)))).
+    destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; auto.
+    destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
+    rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
+    rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
+    rewrite Int.translate_cmpu
+      by eauto using Mem.weak_valid_pointer_inject_no_overflow.
+    apply val_inject_val_of_optbool.
     (* different source blocks *)
+    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; auto.
+    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
     destruct (zeq b2 b3).
-    exploit Mem.different_pointers_inject; eauto. intros [A|A]. 
-    congruence.
-    destruct c; simpl; auto. 
+    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
+    fold (Mem.weak_valid_pointer tm b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))).
+    rewrite Mem.valid_pointer_implies
+      by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb); eauto).
+    rewrite Mem.valid_pointer_implies
+      by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0); eauto).
+    exploit Mem.different_pointers_inject; eauto. intros [A|A]; [congruence |].
+    destruct c; simpl; auto.
     rewrite Int.eq_false. constructor. congruence.
     rewrite Int.eq_false. constructor. congruence.
+    rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
+    rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
     apply val_inject_val_of_optbool.
   (* cmpf *)
   inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.