From e884946c8788db4eb791fa93761d487b9de13ae4 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 29 Oct 2010 14:21:59 +0000 Subject: float->int conversions, continued: weaker axiomatization. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1545 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Floats.v | 25 +++---------------------- 1 file changed, 3 insertions(+), 22 deletions(-) (limited to 'lib') diff --git a/lib/Floats.v b/lib/Floats.v index 50712af..f6af7bf 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -31,8 +31,6 @@ Parameter zero: float. (**r the float [+0.0] *) Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}. -Parameter of_Z: Z -> float. (**r conversion from exact integers, for specification *) - (** Arithmetic operations *) Parameter neg: float -> float. (**r opposite (change sign) *) @@ -118,18 +116,6 @@ Axiom bits_of_singleoffloat: Axiom singleoffloat_of_bits: forall b, singleoffloat (single_of_bits b) = single_of_bits b. -(** Range of conversions from floats to ints. *) - -Axiom intuoffloat_defined: - forall f, - cmp Clt f (of_Z Int.modulus) = true /\ cmp Cge f zero = true - <-> exists n, intuoffloat f = Some n. - -Axiom intoffloat_defined: - forall f, - cmp Clt f (of_Z Int.half_modulus) = true /\ cmp Cgt f (of_Z (- Int.half_modulus - 1)) = true - <-> exists n, intoffloat f = Some n. - (** Conversions between floats and unsigned ints can be defined in terms of conversions between floats and signed ints. (Most processors provide only the latter, forcing the compiler @@ -149,9 +135,10 @@ Axiom floatofintu_floatofint_2: (floatofintu ox8000_0000). Axiom intuoffloat_intoffloat_1: - forall x, + forall x n, cmp Clt x (floatofintu ox8000_0000) = true -> - intuoffloat x = intoffloat x. + intuoffloat x = Some n -> + intoffloat x = Some n. Axiom intuoffloat_intoffloat_2: forall x n, @@ -159,12 +146,6 @@ Axiom intuoffloat_intoffloat_2: intuoffloat x = Some n -> intoffloat (sub x (floatofintu ox8000_0000)) = Some (Int.sub n ox8000_0000). -Axiom intuoffloat_intoffloat_3: - forall x n, - cmp Clt x (floatofintu ox8000_0000) = false -> - intoffloat (sub x (floatofintu ox8000_0000)) = Some n -> - intuoffloat x = Some (Int.add n ox8000_0000). - (** Conversions from ints to floats can be defined as bitwise manipulations over the in-memory representation. This is what the PowerPC port does. The trick is that [from_words 0x4330_0000 x] is the float -- cgit v1.2.3