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 /lib | |
| parent | d71a5cfd10378301b71d32659d5936e01d72ae50 (diff) | |
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 'lib')
| -rw-r--r-- | lib/Floats.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 50298f7..5c20cdd 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: |