From d71a5cfd10378301b71d32659d5936e01d72ae50 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 9 May 2010 08:18:51 +0000 Subject: Revised encoding/decoding of floats git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Floats.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'lib/Floats.v') 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. -- cgit