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/Cshmgenproof.v | |
| parent | f1ceca440c0322001abe6c5de79bd4bc309fc002 (diff) | |
| download | compcert-kvx-f774d5f2d604f747e72e2d3bb56cc3f90090e2dd.tar.gz compcert-kvx-f774d5f2d604f747e72e2d3bb56cc3f90090e2dd.zip | |
Pointers one past
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 74a6da5e..ad5ada64 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -574,7 +574,8 @@ Proof. inversion H8. eauto with cshm. (* pp ptr ptr *) inversion H10. eapply eval_Ebinop; eauto with cshm. - simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9. auto. + simpl. unfold Val.cmpu. simpl. unfold Mem.weak_valid_pointer in *. + rewrite H3. rewrite H9. auto. inversion H10. eapply eval_Ebinop; eauto with cshm. simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9. destruct cmp; simpl in *; inv H; auto. |