Treat casts int64 -> float32 as primitive operations instead of two

casts int64 -> float64 -> float32.  The latter causes double rounding
errors.


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

1 files changed, 5 insertions, 0 deletions

diff --git a/test/regression/int64.c b/test/regression/int64.c
index 5b32ccd..0012216 100644
--- a/test/regression/int64.c
+++ b/test/regression/int64.c
@@ -38,6 +38,7 @@ static void test1(u64 x, u64 y)
   s64 y3;
   int i;
   double f;
+  float s;
 
   printf("x = %llx\n", x);
   printf("y = %llx\n", y);
@@ -75,6 +76,10 @@ static void test1(u64 x, u64 y)
   printf("stod x = %llx\n", *((u64*) &f));
   f = f * 0.0001;
   printf("dtos f = %llx\n", (s64) f);
+  s = (float) x;
+  printf("utof x = %x\n", *((unsigned*) &s));
+  s = (float) ((s64) x);
+  printf("stof x = %x\n", *((unsigned*) &s));
   printf("\n");
 }