Revised handling of int->float conversions:

- introduce Float.floatofint{,u} and use it in the semantics of C
- prove that it is equivalent to int->double conversion followed by
  double->float rounding, and use this fact to justify code generation
  in Cshmgen.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2294 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 5 deletions

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 1148d09d..a1860ec0 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -127,10 +127,12 @@ Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
   | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one
   end.
 
-Definition cast_int_float (si : signedness) (i: int) : float :=
-  match si with
-  | Signed => Float.floatofint i
-  | Unsigned => Float.floatofintu i
+Definition cast_int_float (si: signedness) (sz: floatsize) (i: int) : float :=
+  match si, sz with
+  | Signed, F64 => Float.floatofint i
+  | Unsigned, F64 => Float.floatofintu i
+  | Signed, F32 => Float.singleofint i
+  | Unsigned, F32 => Float.singleofintu i
   end.
 
 Definition cast_float_int (si : signedness) (f: float) : option int :=
@@ -184,7 +186,7 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
       end
   | cast_case_i2f si1 sz2 =>
       match v with
-      | Vint i => Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
+      | Vint i => Some (Vfloat (cast_int_float si1 sz2 i))
       | _ => None
       end
   | cast_case_f2i sz2 si2 =>