From 39bc6e4f98dabf672798893df990576542ac1675 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 29 Mar 2014 08:30:03 +0000 Subject: __builtin_absfloat can be applied to integers too. More precise classification of float results of arithmetic operations, in preparation for future work on the C/Clight static type system. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2441 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index d6e881e7..15c4e4cd 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -348,6 +348,17 @@ Proof. destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm. Qed. +Lemma make_absfloat_correct: + forall a tya c va v e le m, + sem_absfloat va tya = Some v -> + make_absfloat a tya = OK c -> + eval_expr ge e le m a va -> + eval_expr ge e le m c v. +Proof. + unfold sem_absfloat, make_absfloat; intros until m; intros SEM MAKE EV1; + destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm. +Qed. + Lemma make_notbool_correct: forall a tya c va v e le m, sem_notbool va tya = Some v -> @@ -621,7 +632,7 @@ Proof. eapply make_notbool_correct; eauto. eapply make_notint_correct; eauto. eapply make_neg_correct; eauto. - inv H. unfold sem_absfloat in H0. destruct va; inv H0. eauto with cshm. + eapply make_absfloat_correct; eauto. Qed. Lemma transl_binop_correct: -- cgit