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, 15 insertions, 7 deletions

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);