From e4585d1b9523c174c75518546513e8184587639d Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 9 May 2010 09:51:23 +0000
Subject: [PATCH] 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
---
cfrontend/Csem.v | 7 ++++---
cfrontend/Cshmgenproof2.v | 12 ++++--------
lib/Floats.v | 3 ---
3 files changed, 8 insertions(+), 14 deletions(-)
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 6e35c2f04..5f8bbf140 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -40,8 +40,9 @@ Inductive is_false: val -> type -> Prop :=
is_false (Vint Int.zero) (Tint sz sg)
| is_false_pointer: forall t,
is_false (Vint Int.zero) (Tpointer t)
- | is_false_float: forall sz,
- is_false (Vfloat Float.zero) (Tfloat sz).
+ | is_false_float: forall sz f,
+ Float.cmp Ceq f Float.zero = true ->
+ is_false (Vfloat f) (Tfloat sz).
Inductive is_true: val -> type -> Prop :=
| is_true_int_int: forall n sz sg,
@@ -55,7 +56,7 @@ Inductive is_true: val -> type -> Prop :=
| is_true_pointer_pointer: forall b ofs t,
is_true (Vptr b ofs) (Tpointer t)
| is_true_float: forall f sz,
- f <> Float.zero ->
+ Float.cmp Ceq f Float.zero = false ->
is_true (Vfloat f) (Tfloat sz).
Inductive bool_of_val : val -> type -> val -> Prop :=
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 3f0f4b3ee..e58570b62 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.
diff --git a/lib/Floats.v b/lib/Floats.v
index 50298f707..5c20cdd63 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -70,9 +70,6 @@ Axiom cmp_le_lt_eq:
Axiom cmp_ge_gt_eq:
forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2.
-Axiom eq_zero_true: cmp Ceq zero zero = true.
-Axiom eq_zero_false: forall f, f <> zero -> cmp Ceq f zero = false.
-
Axiom bits_of_double_of_bits:
forall n, bits_of_double (double_of_bits n) = n.
Axiom double_of_bits_of_double:
--
GitLab