diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-03-29 08:30:03 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-03-29 08:30:03 +0000 |
| commit | 39bc6e4f98dabf672798893df990576542ac1675 (patch) | |
| tree | b8f5e1894c06ab3dc70772771ec0652ab12cbe36 /cfrontend/Cshmgenproof.v | |
| parent | 3ad2cfa6013d73f0af95af51a4b72c826478773a (diff) | |
__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
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index d6e881e..15c4e4c 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: |