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 /ia32/Asmgenproof1.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 'ia32/Asmgenproof1.v')
| -rw-r--r-- | ia32/Asmgenproof1.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 7a4348b..b524539 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -1110,10 +1110,11 @@ Proof. rewrite Heqb1; reflexivity. (* ptr ptr *) simpl. - destruct (Mem.valid_pointer m b0 (Int.unsigned i) && - Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate. + fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *. + fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *. destruct (zeq b0 b1). - inversion H1. + destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) && + Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1. destruct c; simpl; auto. destruct (Int.eq i i0); reflexivity. destruct (Int.eq i i0); auto. @@ -1121,6 +1122,8 @@ Proof. rewrite int_not_ltu. destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto. rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. destruct (Int.ltu i i0); reflexivity. + destruct (Mem.valid_pointer m b0 (Int.unsigned i) && + Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate. destruct c; simpl in *; inv H1; reflexivity. Qed. |