From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 23 Jul 2014 08:54:56 +0000
Subject: Merge of "newspilling" branch: - Support single-precision floats as
 first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64
 to   support saving and restoring registers without knowing   the exact types
 (int/single/float) of their contents, just   their sizes. - Memory model:
 generalize the opaque encoding of pointers to   apply to any value, not just
 pointers, if chunks Many32/Many64   are selected. - More properties of FP
 arithmetic proved.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 test/c/fftsp.c          | 12 ++++++------
 test/regression/NaNs.c  | 48 ++++++++++++++++++++++++++++++++++++++++++------
 test/spass/Makefile.bak | 13 -------------
 3 files changed, 48 insertions(+), 25 deletions(-)
 delete mode 100644 test/spass/Makefile.bak

(limited to 'test')

diff --git a/test/c/fftsp.c b/test/c/fftsp.c
index 42ae905..3c7c23c 100644
--- a/test/c/fftsp.c
+++ b/test/c/fftsp.c
@@ -52,17 +52,17 @@ int dfft(float x[], float y[], int np)
   for (k = 1;  k <= m-1; k++ ) {
     n2 = n2 / 2; 
     n4 = n2 / 4; 
-    e  = tpi / (double)n2; 
+    e  = tpi / (float)n2; 
     a  = 0.0;
     
     for (j = 1; j<= n4 ; j++) {
-      a3 = 3.0 * a; 
+      a3 = 3.0f * a; 
       cc1 = cosf(a); 
       ss1 = sinf(a);
       
       cc3 = cosf(a3); 
       ss3 = sinf(a3); 
-      a = e * (double)j; 
+      a = e * (float)j; 
       is = j; 
       id = 2 * n2;
 	  
@@ -162,7 +162,7 @@ int main(int argc, char ** argv)
   xi = calloc(np, sizeof(float));
   pxr = xr;
   pxi = xi;
-  *pxr = (enp - 1.0) * 0.5;
+  *pxr = (enp - 1.0) * 0.5f;
   *pxi = 0.0;
   n2 = np / 2;  
   *(pxr+n2) = -0.5;
@@ -171,8 +171,8 @@ int main(int argc, char ** argv)
     j = np - i;
     *(pxr+i) = -0.5;
     *(pxr+j) = -0.5;
-    z = t * (double)i;  
-    y = -0.5*(cosf(z)/sinf(z));
+    z = t * (float)i;  
+    y = -0.5f*(cosf(z)/sinf(z));
     *(pxi+i) =  y;
     *(pxi+j) = -y;
   }
diff --git a/test/regression/NaNs.c b/test/regression/NaNs.c
index 45f1e7f..618ce29 100644
--- a/test/regression/NaNs.c
+++ b/test/regression/NaNs.c
@@ -32,17 +32,17 @@ inline float single_of_bits(u32 i)
   u.i = i; return u.f;
 }
 
-volatile double val[8];
-
 char * valname[8] = {
   "+0", "-0", "+inf", "-inf",
   "snan(5)", "qnan(6)", "snan(-9)", "qnan(-1)"
 };
 
-int main()
+void test64(void)
 {
+  volatile double val[8];
   int i, j;
 
+  printf("--- Double precision\n");
   val[0] = 0.0;
   val[1] = - val[0];
   val[2] = double_of_bits(0x7FF0000000000000);
@@ -56,10 +56,7 @@ int main()
   for (i = 0; i < 8; i++) {
     printf("opp(%s) = 0x%016llx\n", valname[i], bits_of_double(- val[i]));
     printf("single(%s) = 0x%08x\n", valname[i], bits_of_single((float)(val[i])));
-#if 0
-    /* The reference interpreter doesn't support __builtin_fabs */
     printf("abs(%s) = 0x%016llx\n", valname[i], bits_of_double(__builtin_fabs(val[i])));
-#endif
     for (j = 0; j < 8; j++) {
       printf("%s + %s = 0x%016llx\n",
              valname[i], valname[j], bits_of_double(val[i] + val[j]));
@@ -71,5 +68,44 @@ int main()
              valname[i], valname[j], bits_of_double(val[i] / val[j]));
     }
   }
+}
+
+void test32(void)
+{
+  volatile float val[8];
+  int i, j;
+
+  printf("--- Single precision\n");
+  val[0] = 0.0f;
+  val[1] = - val[0];
+  val[2] = single_of_bits(0x7F800000);
+  val[3] = - val[2];
+
+  val[4] = single_of_bits(0x7F800005);
+  val[5] = single_of_bits(0x7FC00006);
+  val[6] = single_of_bits(0xFF800009);
+  val[7] = single_of_bits(0xFFC00001);
+
+  for (i = 0; i < 8; i++) {
+    printf("opp(%s) = 0x%08x\n", valname[i], bits_of_single(- val[i]));
+    printf("double(%s) = 0x%016llx\n", valname[i], bits_of_double((double)(val[i])));
+    printf("abs(%s) = 0x%08x\n", valname[i], bits_of_single(__builtin_fabs(val[i])));
+    for (j = 0; j < 8; j++) {
+      printf("%s + %s = 0x%08x\n",
+             valname[i], valname[j], bits_of_single(val[i] + val[j]));
+      printf("%s - %s = 0x%08x\n",
+             valname[i], valname[j], bits_of_single(val[i] - val[j]));
+      printf("%s * %s = 0x%08x\n",
+             valname[i], valname[j], bits_of_single(val[i] * val[j]));
+      printf("%s / %s = 0x%08x\n",
+             valname[i], valname[j], bits_of_single(val[i] / val[j]));
+    }
+  }
+}
+
+int main(void)
+{
+  test64();
+  test32();
   return 0;
 }
diff --git a/test/spass/Makefile.bak b/test/spass/Makefile.bak
deleted file mode 100644
index 320f622..0000000
--- a/test/spass/Makefile.bak
+++ /dev/null
@@ -1,13 +0,0 @@
-LEVEL = ../../..
-PROG = SPASS
-
-CPPFLAGS = -DCLOCK_NO_TIMING -fno-strict-aliasing -w
-LDFLAGS  = -lm
-
-ifdef SMALL_PROBLEM_SIZE
-RUN_OPTIONS="$(PROJ_SRC_DIR)/small_problem.dfg"
-else
-RUN_OPTIONS="$(PROJ_SRC_DIR)/problem.dfg"
-endif
-
-include ../../Makefile.multisrc
-- 
cgit v1.2.3