diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-09 08:18:51 +0000 |
commit | d71a5cfd10378301b71d32659d5936e01d72ae50 (patch) | |
tree | 9b6a7cc437ab205b7e0bf5bf90585451d8a8c367 /lib/Floats.v | |
parent | 913c1bcc4b2204afd447edd723e06b905fd1f47f (diff) | |
download | compcert-kvx-d71a5cfd10378301b71d32659d5936e01d72ae50.tar.gz compcert-kvx-d71a5cfd10378301b71d32659d5936e01d72ae50.zip |
Revised encoding/decoding of floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Floats.v')
-rw-r--r-- | lib/Floats.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 2e60d73e..50298f70 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -47,6 +47,12 @@ Parameter cmp: comparison -> float -> float -> bool. Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}. +Parameter bits_of_double: float -> int64. +Parameter double_of_bits: int64 -> float. + +Parameter bits_of_single: float -> int. +Parameter single_of_bits: int -> float. + (** Below are the only properties of floating-point arithmetic that we rely on in the compiler proof. *) @@ -67,4 +73,16 @@ Axiom cmp_ge_gt_eq: 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: + forall f, double_of_bits (bits_of_double f) = f. +Axiom bits_of_single_of_bits: + forall n, bits_of_single (single_of_bits n) = n. +Axiom single_of_bits_of_single: + forall f, single_of_bits (bits_of_single f) = singleoffloat f. + +Axiom bits_of_singleoffloat: + forall f, bits_of_single (singleoffloat f) = bits_of_single f. + End Float. |