From b9eef9995d212255ee1fa94877ca891aee6adfc3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 13 Nov 2007 14:49:02 +0000 Subject: In Clight, revised handling of comparisons between pointers and 0 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@447 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof2.v | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) (limited to 'cfrontend/Cshmgenproof2.v') diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index aa4e391a..6b7b5e3c 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -285,15 +285,24 @@ Lemma make_cmp_correct: eval_expr tprog e m c v. Proof. intros until m. intro SEM. unfold make_cmp. - functional inversion SEM; rewrite H0; intros. - inversion H8. eauto with cshm. + functional inversion SEM; rewrite H0; intros. + (* I32unsi *) inversion H8. eauto with cshm. + (* ipip int int *) inversion H8. eauto with cshm. - inversion H9. eapply eval_Ebinop; eauto with cshm. - simpl. functional inversion H; subst; unfold eval_compare_null; - rewrite H8; auto. + (* ipip ptr ptr *) inversion H10. eapply eval_Ebinop; eauto with cshm. - simpl. rewrite H3. unfold eq_block; rewrite H9. auto. + simpl. rewrite H3. unfold eq_block. rewrite H9. auto. + (* ipip ptr int *) + inversion H9. eapply eval_Ebinop; eauto with cshm. + simpl. unfold eval_compare_null. rewrite H8. + functional inversion H; subst; auto. + (* ipip int ptr *) + inversion H9. eapply eval_Ebinop; eauto with cshm. + simpl. unfold eval_compare_null. rewrite H8. + functional inversion H; subst; auto. + (* ff *) + inversion H8. eauto with cshm. Qed. Lemma transl_unop_correct: -- cgit