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

1 files changed, 27 insertions, 0 deletions

diff --git a/test/cminor/lists.cm b/test/cminor/lists.cm
new file mode 100644
index 00000000..c4456236
--- /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];
+  }
+}
+