diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 09:51:23 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 09:51:23 +0000 |
| commit | e4585d1b9523c174c75518546513e8184587639d (patch) | |
| tree | 5d420b18233d4a327f482f670519631a04e2f2c4 /cfrontend/Cshmgenproof2.v | |
| parent | d71a5cfd10378301b71d32659d5936e01d72ae50 (diff) | |
| download | compcert-e4585d1b9523c174c75518546513e8184587639d.tar.gz compcert-e4585d1b9523c174c75518546513e8184587639d.zip | |
Suppressed axioms Float.eq_zero_{true,false}, since the latter is
wrong because of +0.0 / -0.0.
Adapted Clight semantics accordingly. (Truth value of a float is
defined by comparison Float.cmp Ceq with 0.0, no longer by structural
equality.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgenproof2.v')
| -rw-r--r-- | cfrontend/Cshmgenproof2.v | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index 3f0f4b3e..e58570b6 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -78,10 +78,8 @@ Proof. try (exists v; intuition; inversion VTRUE; simpl; auto; fail). exists Vtrue; split. eapply eval_Ebinop; eauto with cshm. - inversion VTRUE; simpl. - replace (Float.cmp Cne f0 Float.zero) with (negb (Float.cmp Ceq f0 Float.zero)). - rewrite Float.eq_zero_false. reflexivity. auto. - rewrite Float.cmp_ne_eq. auto. + inversion VTRUE; simpl. + rewrite Float.cmp_ne_eq. rewrite H1. auto. apply Vtrue_is_true. Qed. @@ -98,10 +96,8 @@ Proof. try (exists v; intuition; inversion VFALSE; simpl; auto; fail). exists Vfalse; split. eapply eval_Ebinop; eauto with cshm. - inversion VFALSE; simpl. - replace (Float.cmp Cne Float.zero Float.zero) with (negb (Float.cmp Ceq Float.zero Float.zero)). - rewrite Float.eq_zero_true. reflexivity. - rewrite Float.cmp_ne_eq. auto. + inversion VFALSE; simpl. + rewrite Float.cmp_ne_eq. rewrite H1. auto. apply Vfalse_is_false. Qed. |