From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: 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 --- caml/Allocationaux.ml | 39 --------------------------------------- 1 file changed, 39 deletions(-) delete mode 100644 caml/Allocationaux.ml (limited to 'caml/Allocationaux.ml') 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 -- cgit