From f774d5f2d604f747e72e2d3bb56cc3f90090e2dd Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Feb 2013 16:24:13 +0000 Subject: Pointers one past git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'cfrontend/Cshmgenproof.v') 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. -- cgit