diff options
author | 2007-11-13 14:49:02 +0000 | |
---|---|---|
committer | 2007-11-13 14:49:02 +0000 | |
commit | b9eef9995d212255ee1fa94877ca891aee6adfc3 (patch) | |
tree | 8cf5eff91187ece3036f071f510db2e7e1b736a6 /cfrontend/Cshmgenproof2.v | |
parent | 3db50bce2c4f3178da9bcc8baac167540ca89019 (diff) |
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
Diffstat (limited to 'cfrontend/Cshmgenproof2.v')
-rw-r--r-- | cfrontend/Cshmgenproof2.v | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index aa4e391..6b7b5e3 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: |