Fusion de la branche "traces":

- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.


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

5 files changed, 73 insertions, 26 deletions

diff --git a/test/cminor/Makefile b/test/cminor/Makefile
index 35d3e07..f9b863e 100644
--- a/test/cminor/Makefile
+++ b/test/cminor/Makefile
@@ -1,10 +1,11 @@
 CCOMP=../../ccomp
 CPP=cpp -P
 CC=gcc
-CFLAGS=-g
+CFLAGS=-arch ppc -g
+ASFLAGS=-arch ppc
 VPATH=../harness ../lib
 
-PROGS=fib integr qsort fft sha1 aes almabench manyargs
+PROGS=fib integr qsort fft sha1 aes almabench manyargs lists
 
 all_s: $(PROGS:%=%.s)
 
@@ -27,13 +28,13 @@ qsort: qsort.o mainqsort.o
 clean::
 	rm -f qsort
 
-fft: fft.o mainfft.o staticlib.o
-	$(CC) $(CFLAGS) -o fft fft.o mainfft.o staticlib.o -lm
+fft: fft.o mainfft.o
+	$(CC) $(CFLAGS) -o fft fft.o mainfft.o -lm
 clean::
 	rm -f fft
 
-sha1: sha1.o mainsha1.o staticlib.o
-	$(CC) $(CFLAGS) -o sha1 sha1.o mainsha1.o staticlib.o
+sha1: sha1.o mainsha1.o
+	$(CC) $(CFLAGS) -o sha1 sha1.o mainsha1.o
 clean::
 	rm -f sha1 sha1.cm
 
@@ -42,8 +43,8 @@ aes: aes.o mainaes.o
 clean::
 	rm -f aes aes.cm
 
-almabench: almabench.o mainalmabench.o staticlib.o
-	$(CC) $(CFLAGS) -o almabench almabench.o mainalmabench.o staticlib.o -lm
+almabench: almabench.o mainalmabench.o
+	$(CC) $(CFLAGS) -o almabench almabench.o mainalmabench.o -lm
 clean::
 	rm -f almabench almabench.cm
 
@@ -52,6 +53,11 @@ manyargs: manyargs.o mainmanyargs.o
 clean::
 	rm -f manyargs
 
+lists: lists.o mainlists.o
+	$(CC) $(CFLAGS) -o lists lists.o mainlists.o
+clean::
+	rm -f lists
+
 .SUFFIXES:
 
 .SUFFIXES: .cmp .cm .s .o .c .S
diff --git a/test/cminor/almabench.cmp b/test/cminor/almabench.cmp
index e9e8392..bafcb5d 100644
--- a/test/cminor/almabench.cmp
+++ b/test/cminor/almabench.cmp
@@ -28,12 +28,20 @@
 #define sl(x,y) float64["sl" + ((x) * 80 + (y) * 8)]
 
 /* Function calls */
-#define cos(x) ("cos_static"(x): float -> float)
-#define sin(x) ("sin_static"(x): float -> float)
-#define atan2(x,y) ("atan2_static"(x,y): float -> float -> float)
-#define asin(x) ("asin_static"(x): float -> float)
-#define sqrt(x) ("sqrt_static"(x): float -> float)
-#define fmod(x,y) ("fmod_static"(x,y): float -> float -> float)
+
+extern "cos": float -> float
+extern "sin": float -> float
+extern "atan2": float -> float -> float
+extern "asin": float -> float
+extern "sqrt": float -> float
+extern "fmod": float -> float -> float
+
+#define cos(x) ("cos"(x): float -> float)
+#define sin(x) ("sin"(x): float -> float)
+#define atan2(x,y) ("atan2"(x,y): float -> float -> float)
+#define asin(x) ("asin"(x): float -> float)
+#define sqrt(x) ("sqrt"(x): float -> float)
+#define fmod(x,y) ("fmod"(x,y): float -> float -> float)
 #define anpm(x) ("anpm"(x) : float -> float)
 
 "anpm"(a): float -> float
@@ -90,7 +98,7 @@
         k = k + 1;
     } }}
 
-    dl = "fmod_static"(dl,TWOPI) : float -> float -> float;
+    dl = "fmod"(dl,TWOPI) : float -> float -> float;
 
     am = dl -f dp;
     ae = am +f de *f sin(am);
diff --git a/test/cminor/fft.cm b/test/cminor/fft.cm
index b4e6a40..ed3b103 100644
--- a/test/cminor/fft.cm
+++ b/test/cminor/fft.cm
@@ -5,6 +5,9 @@
 /*     Length is n.                                     */
 /********************************************************/
 
+extern "cos" : float -> float
+extern "sin" : float -> float
+
 "dfft"(x, y, np): int /*float ptr*/ -> int /*float ptr*/ -> int -> int
 {
   var px, py, /*float ptr*/
@@ -48,11 +51,11 @@
     j = 1;
     {{ loop {
       if (! (j <= n4)) exit;
-      cc1 = "cos_static"(a) : float -> float; 
-      ss1 = "sin_static"(a) : float -> float;
+      cc1 = "cos"(a) : float -> float; 
+      ss1 = "sin"(a) : float -> float;
       a3 = 3.0 *f a; 
-      cc3 = "cos_static"(a3) : float -> float; 
-      ss3 = "sin_static"(a3) : float -> float; 
+      cc3 = "cos"(a3) : float -> float; 
+      ss3 = "sin"(a3) : float -> float; 
       a = e *f floatofint(j);
       is = j; 
       id = 2 * n2;
diff --git a/test/cminor/lists.cm b/test/cminor/lists.cm
new file mode 100644
index 0000000..c445623
--- /dev/null
+++ b/test/cminor/lists.cm
@@ -0,0 +1,27 @@
+/* List manipulations */
+
+"buildlist"(n): int -> int
+{
+  var b;
+
+  if (n < 0) return 0;
+  b = alloc 8;
+  int32[b] = n;
+  int32[b+4] = "buildlist"(n - 1) : int -> int;
+  return b;
+}
+
+"reverselist"(l): int -> int
+{
+  var r, r2;
+  r = 0;
+  loop {
+    if (l == 0) return r;
+    r2 = alloc 8;
+    int32[r2] = int32[l];
+    int32[r2+4] = r;
+    r = r2;
+    l = int32[l+4];
+  }
+}
+
diff --git a/test/cminor/sha1.cmp b/test/cminor/sha1.cmp
index 9a588e4..ca24544 100644
--- a/test/cminor/sha1.cmp
+++ b/test/cminor/sha1.cmp
@@ -3,6 +3,9 @@
 
 /* To be preprocessed by cpp -P */
 
+extern "memcpy" : int -> int -> int -> void
+extern "memset" : int -> int -> int -> void
+
 #define ARCH_BIG_ENDIAN
 
 #define rol1(x) (((x) << 1) | ((x) >>u 31))
@@ -12,7 +15,7 @@
 "SHA1_copy_and_swap"(src, dst, numwords) : int -> int -> int -> void
 {
 #ifdef ARCH_BIG_ENDIAN
-  "memcpy_static"(dst, src, numwords * 4) : int -> int -> int -> void;
+  "memcpy"(dst, src, numwords * 4) : int -> int -> int -> void;
 #else
   var s, d, a, b;
   s = src;
@@ -134,12 +137,12 @@
   if (context_numbytes(ctx) != 0) {
     t = 64 - context_numbytes(ctx);
     if (len <u t) {
-      "memcpy_static"(context_buffer(ctx) + context_numbytes(ctx), data, len)
+      "memcpy"(context_buffer(ctx) + context_numbytes(ctx), data, len)
         : int -> int -> int -> void;
       context_numbytes(ctx) = context_numbytes(ctx) + len;
       return;
     }
-    "memcpy_static"(context_buffer(ctx) + context_numbytes(ctx), data, t)
+    "memcpy"(context_buffer(ctx) + context_numbytes(ctx), data, t)
         : int -> int -> int -> void;
     "SHA1_transform"(ctx) : int -> void;
     data = data + t;
@@ -148,14 +151,14 @@
   /* Munge data in 64-byte chunks */
   {{ loop {
     if (! (len >=u 64)) exit;
-    "memcpy_static"(context_buffer(ctx), data, 64)
+    "memcpy"(context_buffer(ctx), data, 64)
         : int -> int -> int -> void;
     "SHA1_transform"(ctx) : int -> void;
     data = data + 64;
     len = len - 64;
   } }}
   /* Save remaining data */
-  "memcpy_static"(context_buffer(ctx), data, len)
+  "memcpy"(context_buffer(ctx), data, len)
         : int -> int -> int -> void;
   context_numbytes(ctx) = len;
 }
@@ -170,13 +173,13 @@
   /* If we do not have room for the length (8 bytes), pad to 64 bytes
      with zeroes and munge the data block */
   if (i > 56) {
-    "memset_static"(context_buffer(ctx) + i, 0, 64 - i)
+    "memset"(context_buffer(ctx) + i, 0, 64 - i)
         : int -> int -> int -> void;
     "SHA1_transform"(ctx) : int -> void;
     i = 0;
   }
   /* Pad to byte 56 with zeroes */
-  "memset_static"(context_buffer(ctx) + i, 0, 56 - i)
+  "memset"(context_buffer(ctx) + i, 0, 56 - i)
         : int -> int -> int -> void;
   /* Add length in big-endian */
   "SHA1_copy_and_swap"(context_length(ctx), context_buffer(ctx) + 56, 2)