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

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;