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, 0 insertions, 39 deletions

diff --git a/caml/Allocationaux.ml b/caml/Allocationaux.ml
deleted file mode 100644
index c682c3c1..00000000
--- a/caml/Allocationaux.ml
+++ /dev/null
@@ -1,39 +0,0 @@
-open Camlcoq
-open Datatypes
-open CList
-open AST
-open Locations
-
-type status = To_move | Being_moved | Moved
-
-let parallel_move_order lsrc ldst =
-  let src = array_of_coqlist lsrc
-  and dst = array_of_coqlist ldst in
-  let n = Array.length src in
-  let status = Array.make n To_move in
-  let moves = ref Coq_nil in
-  let rec move_one i =
-    if src.(i) <> dst.(i) then begin
-      status.(i) <- Being_moved;
-      for j = 0 to n - 1 do
-        if src.(j) = dst.(i) then
-          match status.(j) with
-            To_move ->
-              move_one j
-          | Being_moved ->
-              let tmp =
-                match Loc.coq_type src.(j) with
-                | Tint -> R IT2
-                | Tfloat -> R FT2 in
-              moves := Coq_cons (Coq_pair(src.(j), tmp), !moves);
-              src.(j) <- tmp
-          | Moved ->
-              ()
-      done;
-      moves := Coq_cons(Coq_pair(src.(i), dst.(i)), !moves);
-      status.(i) <- Moved
-    end in
-  for i = 0 to n - 1 do
-    if status.(i) = To_move then move_one i
-  done;
-  CList.rev !moves