Problemes d'alignement des variables globales et a l'interieur de leurs initialiseurs

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@444 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

7 files changed, 234 insertions, 166 deletions

diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index 0e168414..fd3ad496 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -796,50 +796,67 @@ let init_data_of_string s =
   done;
   !id
 
-let rec convertInit init k =
-  match init with
-  | SingleInit e ->
-      begin match extract_constant(Cil.constFold true e) with
-      | ICint(n, I8) ->
-          CList.Coq_cons(Init_int8 (coqint_of_camlint (Int64.to_int32 n)), k)
-      | ICint(n, I16) ->
-          CList.Coq_cons(Init_int16 (coqint_of_camlint (Int64.to_int32 n)), k)
-      | ICint(n, I32) ->
-          CList.Coq_cons(Init_int32 (coqint_of_camlint (Int64.to_int32 n)), k)
-      | ICfloat(n, F32) ->
-          CList.Coq_cons(Init_float32 n, k)
-      | ICfloat(n, F64) ->
-          CList.Coq_cons(Init_float64 n, k)
-      | ICstring s ->
-          CList.Coq_cons(Init_pointer(init_data_of_string s), k)
-      | ICnone ->
-          unsupported "this kind of expression is not supported in global initializers"
-    end
-  | CompoundInit(ty, data) ->
-      begin match Cil.unrollType ty with
-      | TComp _ ->
-          let init =
-            Cil.foldLeftCompoundAll
-              ~doinit: (fun ofs init ty k -> convertInit init k)
-              ~ct: ty
-              ~initl: data
-              ~acc: CList.Coq_nil in
-          let act_len = initDataLen 0l init in
-          let exp_len = camlint_of_z (Csyntax.sizeof (convertTyp ty)) in
-          assert (act_len <= exp_len);
-          let init' = 
-            if act_len < exp_len
-            then let spc = z_of_camlint (Int32.sub exp_len act_len) in
-                 CList.Coq_cons(Init_space spc, init)
-            else init in
-          CList.app init' k
-      | _ ->
-          Cil.foldLeftCompoundAll
-            ~doinit: (fun ofs init ty k -> convertInit init k)
-            ~ct: ty
-            ~initl: data
-            ~acc: k
+let convertInit init =
+  let k = ref Coq_nil
+  and pos = ref 0 in
+  let emit size datum =
+    k := Coq_cons(datum, !k);
+    pos := !pos + size in
+  let emit_space size =
+    emit size (Init_space (z_of_camlint (Int32.of_int size))) in
+  let check_align size =
+    assert (!pos land (size - 1) = 0) in
+  let align size =
+    let n = !pos land (size - 1) in
+    if n > 0 then emit_space (size - n) in
+
+  let rec cvtInit init =
+    match init with
+    | SingleInit e ->
+        begin match extract_constant(Cil.constFold true e) with
+        | ICint(n, I8) ->
+            let n' = coqint_of_camlint (Int64.to_int32 n) in
+            emit 1 (Init_int8 n')
+        | ICint(n, I16) ->
+            check_align 2;
+            let n' = coqint_of_camlint (Int64.to_int32 n) in
+            emit 2 (Init_int16 n')
+        | ICint(n, I32) ->
+            check_align 4;
+            let n' = coqint_of_camlint (Int64.to_int32 n) in
+            emit 4 (Init_int32 n')
+        | ICfloat(n, F32) ->
+            check_align 4;
+            emit 4 (Init_float32 n)
+        | ICfloat(n, F64) ->
+            check_align 8;
+            emit 8 (Init_float64 n)
+        | ICstring s ->
+            check_align 4;
+            emit 4 (Init_pointer(init_data_of_string s))
+        | ICnone ->
+            unsupported "this kind of expression is not supported in global initializers"
       end
+  | CompoundInit(ty, data) ->
+      let ty' = convertTyp ty in
+      let sz = Int32.to_int (camlint_of_z (Csyntax.sizeof ty')) in
+      let pos0 = !pos in
+      Cil.foldLeftCompoundAll
+          ~doinit: cvtCompoundInit
+          ~ct: ty
+          ~initl: data
+          ~acc: ();
+      let pos1 = !pos in
+      assert (pos1 <= pos0 + sz);
+      if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1)
+
+  and cvtCompoundInit ofs init ty () =
+    let ty' = convertTyp ty in
+    let al = Int32.to_int (camlint_of_z (Csyntax.alignof ty')) in
+    align al;
+    cvtInit init
+
+  in cvtInit init; CList.rev !k
 
 (** Convert a [Cil.initinfo] into a list of [AST.init_data] *)
 
@@ -848,7 +865,7 @@ let convertInitInfo ty info =
   | None -> 
       CList.Coq_cons(Init_space(Csyntax.sizeof (convertTyp ty)), CList.Coq_nil)
   | Some init ->
-      CList.rev (convertInit init CList.Coq_nil)
+      convertInit init
 
 (** Convert a [Cil.GVar] into a global variable definition *)
 
diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml
index 59c42d3b..4eff1c68 100644
--- a/caml/PrintCsyntax.ml
+++ b/caml/PrintCsyntax.ml
@@ -352,7 +352,7 @@ let print_init p = function
   | Init_int32 n -> fprintf p "%ld,@ " (camlint_of_coqint n)
   | Init_float32 n -> fprintf p "%F,@ " n
   | Init_float64 n -> fprintf p "%F,@ " n
-  | Init_space n -> fprintf p "/* skip %ld*/@ " (camlint_of_coqint n)
+  | Init_space n -> fprintf p "/* skip %ld, */@ " (camlint_of_coqint n)
   | Init_pointer id ->
       match string_of_init id with
       | None -> fprintf p "/* pointer to other init*/,@ "
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index bf7b2cc7..97082b9b 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -54,14 +54,10 @@ let print_symb_ofs oc (symb, ofs) =
 let print_constant oc = function
   | Cint n ->
       fprintf oc "%ld" (camlint_of_coqint n)
-  | Csymbol_low_signed(s, n) ->
+  | Csymbol_low(s, n) ->
       fprintf oc "lo16(%a)" print_symb_ofs (s, camlint_of_coqint n)
-  | Csymbol_high_signed(s, n) ->
+  | Csymbol_high(s, n) ->
       fprintf oc "ha16(%a)" print_symb_ofs (s, camlint_of_coqint n)
-  | Csymbol_low_unsigned(s, n) ->
-      fprintf oc "lo16(%a)" print_symb_ofs (s, camlint_of_coqint n)
-  | Csymbol_high_unsigned(s, n) ->
-      fprintf oc "hi16(%a)" print_symb_ofs (s, camlint_of_coqint n)
 
 let num_crbit = function
   | CRbit_0 -> 0
@@ -499,6 +495,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
   | Coq_nil -> ()
   | _  ->
       fprintf oc "	.data\n";
+      fprintf oc "	.align	3\n";
       fprintf oc "	.globl	%a\n" print_symb name;
       fprintf oc "%a:\n" print_symb name;
       print_init_data oc init_data
diff --git a/extraction/.depend b/extraction/.depend
index 60534fdd..62ab7b62 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -4,14 +4,6 @@
 ../caml/Coloringaux.cmi: Registers.cmi RTLtyping.cmi RTL.cmi Locations.cmi \
     InterfGraph.cmi 
 ../caml/PrintPPC.cmi: PPC.cmi 
-../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CString.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi Ascii.cmi 
-../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CString.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx Ascii.cmx 
-../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
-    CList.cmi AST.cmi 
-../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
-    CList.cmx AST.cmx 
 ../caml/CMlexer.cmo: ../caml/Camlcoq.cmo ../caml/CMparser.cmi \
     ../caml/CMlexer.cmi 
 ../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \
@@ -26,6 +18,14 @@
     ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/CMtypecheck.cmi 
 ../caml/CMtypecheck.cmx: Integers.cmx Datatypes.cmx Cminor.cmx \
     ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/CMtypecheck.cmi 
+../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CString.cmi CList.cmi \
+    BinPos.cmi BinInt.cmi Ascii.cmi 
+../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CString.cmx CList.cmx \
+    BinPos.cmx BinInt.cmx Ascii.cmx 
+../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
+    CList.cmi AST.cmi 
+../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
+    CList.cmx AST.cmx 
 ../caml/Coloringaux.cmo: Registers.cmi RTLtyping.cmi RTL.cmi Maps.cmi \
     Locations.cmi InterfGraph.cmi Datatypes.cmi Conventions.cmi \
     ../caml/Camlcoq.cmo BinPos.cmi BinInt.cmi AST.cmi ../caml/Coloringaux.cmi 
@@ -42,10 +42,14 @@
     ../caml/CMlexer.cmx 
 ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo 
 ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx 
-../caml/Linearizeaux.cmo: Maps.cmi Lattice.cmi LTLin.cmi LTL.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi 
-../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTLin.cmx LTL.cmx \
-    Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx 
+../caml/Linearizeaux.cmo: Maps.cmi Lattice.cmi LTL.cmi Datatypes.cmi \
+    Coqlib.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi 
+../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTL.cmx Datatypes.cmx \
+    Coqlib.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx 
+../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
+    ../caml/Camlcoq.cmo CList.cmi AST.cmi 
+../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
+    ../caml/Camlcoq.cmx CList.cmx AST.cmx 
 ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
     CList.cmi AST.cmi 
 ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
@@ -62,12 +66,12 @@
     ../caml/Camlcoq.cmo CList.cmi AST.cmi 
 ../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \
     ../caml/Camlcoq.cmx CList.cmx AST.cmx 
+AST.cmi: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
+    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi 
 Allocation.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi \
     Maps.cmi Locations.cmi LTL.cmi Errors.cmi Datatypes.cmi Coloring.cmi \
     CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi 
 Ascii.cmi: Specif.cmi Peano.cmi Datatypes.cmi Bool.cmi BinPos.cmi 
-AST.cmi: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
-    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi 
 BinInt.cmi: Datatypes.cmi BinPos.cmi BinNat.cmi 
 BinNat.cmi: Specif.cmi Datatypes.cmi BinPos.cmi 
 BinPos.cmi: Peano.cmi Datatypes.cmi 
@@ -76,15 +80,18 @@ Bounds.cmi: Zmax.cmi Locations.cmi Linear.cmi Conventions.cmi CList.cmi \
     BinPos.cmi BinInt.cmi AST.cmi 
 CInt.cmi: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi 
 CList.cmi: Specif.cmi Datatypes.cmi 
-Cminorgen.cmi: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
-    Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi \
-    Cminor.cmi CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi \
-    AST.cmi 
+CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \
+    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
+CString.cmi: Specif.cmi Datatypes.cmi Ascii.cmi 
 Cminor.cmi: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \
     Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi 
 CminorSel.cmi: Values.cmi Op.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi \
     CList.cmi BinInt.cmi AST.cmi 
+Cminorgen.cmi: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
+    Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi \
+    Cminor.cmi CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi \
+    AST.cmi 
 Coloring.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \
     Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
     CList.cmi BinInt.cmi AST.cmi 
@@ -95,15 +102,12 @@ Conventions.cmi: Locations.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
     BinInt.cmi AST.cmi 
 Coqlib.cmi: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \
     BinPos.cmi BinInt.cmi 
-CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \
-    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi 
 Csharpminor.cmi: Zmax.cmi Values.cmi Mem.cmi Maps.cmi Integers.cmi \
     Globalenvs.cmi Floats.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi \
     AST.cmi 
 Cshmgen.cmi: Specif.cmi Peano.cmi Integers.cmi Floats.cmi Errors.cmi \
     Datatypes.cmi Csyntax.cmi Csharpminor.cmi Cminor.cmi CString.cmi \
     CList.cmi Ascii.cmi AST.cmi 
-CString.cmi: Specif.cmi Datatypes.cmi Ascii.cmi 
 Csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Errors.cmi \
     Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi \
     Ascii.cmi AST.cmi 
@@ -111,12 +115,12 @@ Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \
     CList.cmi AST.cmi 
 EqNat.cmi: Specif.cmi Datatypes.cmi 
 Errors.cmi: Datatypes.cmi CString.cmi CList.cmi BinPos.cmi 
-Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi 
 FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Datatypes.cmi \
     CList.cmi CInt.cmi BinPos.cmi BinInt.cmi 
 FSetFacts.cmi: Specif.cmi Setoid.cmi FSetInterface.cmi Datatypes.cmi 
 FSetInterface.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi 
 FSetList.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi 
+Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi 
 Globalenvs.cmi: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \
     CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 Integers.cmi: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \
@@ -127,22 +131,22 @@ Iteration.cmi: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi
 Kildall.cmi: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \
     Lattice.cmi Iteration.cmi Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi \
     BinPos.cmi BinInt.cmi 
+LTL.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
+    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
+    BinPos.cmi BinInt.cmi AST.cmi 
+LTLin.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi 
 Lattice.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
     BinPos.cmi 
-Linearize.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \
-    Lattice.cmi LTLin.cmi LTL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
-    CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
 Linear.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
     Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi 
+Linearize.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \
+    Lattice.cmi LTLin.cmi LTL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
+    CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
 Locations.cmi: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \
     BinInt.cmi AST.cmi 
-LTLin.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi 
-LTL.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
-    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi 
 Mach.cmi: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Locations.cmi \
     Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
     BinInt.cmi AST.cmi 
@@ -159,26 +163,26 @@ Op.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
 Ordered.cmi: Specif.cmi OrderedType.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \
     BinPos.cmi 
 OrderedType.cmi: Specif.cmi Datatypes.cmi 
-Parallelmove.cmi: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi 
-Parmov.cmi: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi 
-Peano.cmi: Datatypes.cmi 
+PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
+    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \
     Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \
     BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
-PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \
-    Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi 
-Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
-    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi 
+Parallelmove.cmi: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi 
+Parmov.cmi: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi 
+Peano.cmi: Datatypes.cmi 
+RTL.cmi: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 RTLgen.cmi: Switch.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi \
     Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CminorSel.cmi \
     CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi 
-RTL.cmi: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Errors.cmi \
     Datatypes.cmi Coqlib.cmi Conventions.cmi CString.cmi CList.cmi BinPos.cmi \
     BinInt.cmi Ascii.cmi AST.cmi 
+Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \
+    Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi 
+Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
+    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi 
 Selection.cmi: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \
     CminorSel.cmi Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi 
 Setoid.cmi: Datatypes.cmi 
@@ -200,6 +204,10 @@ Zeven.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi
 Zmax.cmi: Datatypes.cmi BinInt.cmi 
 Zmisc.cmi: Datatypes.cmi BinPos.cmi BinInt.cmi 
 Zpower.cmi: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi 
+AST.cmo: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
+    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
+AST.cmx: Specif.cmx Integers.cmx Floats.cmx Errors.cmx Datatypes.cmx \
+    Coqlib.cmx CString.cmx CList.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmi 
 Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi \
     Maps.cmi Locations.cmi Lattice.cmi LTL.cmi Kildall.cmi Errors.cmi \
     Datatypes.cmi Coloring.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi \
@@ -210,10 +218,6 @@ Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx Op.cmx \
     AST.cmx Allocation.cmi 
 Ascii.cmo: Specif.cmi Peano.cmi Datatypes.cmi Bool.cmi BinPos.cmi Ascii.cmi 
 Ascii.cmx: Specif.cmx Peano.cmx Datatypes.cmx Bool.cmx BinPos.cmx Ascii.cmi 
-AST.cmo: Specif.cmi Integers.cmi Floats.cmi Errors.cmi Datatypes.cmi \
-    Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi 
-AST.cmx: Specif.cmx Integers.cmx Floats.cmx Errors.cmx Datatypes.cmx \
-    Coqlib.cmx CString.cmx CList.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmi 
 BinInt.cmo: Datatypes.cmi BinPos.cmi BinNat.cmi BinInt.cmi 
 BinInt.cmx: Datatypes.cmx BinPos.cmx BinNat.cmx BinInt.cmi 
 BinNat.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinNat.cmi 
@@ -230,14 +234,14 @@ CInt.cmo: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi CInt.cmi
 CInt.cmx: Zmax.cmx ZArith_dec.cmx Specif.cmx BinPos.cmx BinInt.cmx CInt.cmi 
 CList.cmo: Specif.cmi Datatypes.cmi CList.cmi 
 CList.cmx: Specif.cmx Datatypes.cmx CList.cmi 
-Cminorgen.cmo: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
-    Maps.cmi Integers.cmi FSetAVL.cmi Errors.cmi Datatypes.cmi \
-    Csharpminor.cmi Coqlib.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi \
-    BinInt.cmi Ascii.cmi AST.cmi Cminorgen.cmi 
-Cminorgen.cmx: Zmax.cmx Specif.cmx OrderedType.cmx Ordered.cmx Mem.cmx \
-    Maps.cmx Integers.cmx FSetAVL.cmx Errors.cmx Datatypes.cmx \
-    Csharpminor.cmx Coqlib.cmx Cminor.cmx CString.cmx CList.cmx BinPos.cmx \
-    BinInt.cmx Ascii.cmx AST.cmx Cminorgen.cmi 
+CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \
+    Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
+    AST.cmi CSE.cmi 
+CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Kildall.cmx \
+    Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \
+    AST.cmx CSE.cmi 
+CString.cmo: Specif.cmi Datatypes.cmi Ascii.cmi CString.cmi 
+CString.cmx: Specif.cmx Datatypes.cmx Ascii.cmx CString.cmi 
 Cminor.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \
     Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \
     AST.cmi Cminor.cmi 
@@ -248,6 +252,14 @@ CminorSel.cmo: Values.cmi Op.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi \
     CList.cmi BinInt.cmi AST.cmi CminorSel.cmi 
 CminorSel.cmx: Values.cmx Op.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx \
     CList.cmx BinInt.cmx AST.cmx CminorSel.cmi 
+Cminorgen.cmo: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \
+    Maps.cmi Integers.cmi FSetAVL.cmi Errors.cmi Datatypes.cmi \
+    Csharpminor.cmi Coqlib.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi \
+    BinInt.cmi Ascii.cmi AST.cmi Cminorgen.cmi 
+Cminorgen.cmx: Zmax.cmx Specif.cmx OrderedType.cmx Ordered.cmx Mem.cmx \
+    Maps.cmx Integers.cmx FSetAVL.cmx Errors.cmx Datatypes.cmx \
+    Csharpminor.cmx Coqlib.cmx Cminor.cmx CString.cmx CList.cmx BinPos.cmx \
+    BinInt.cmx Ascii.cmx AST.cmx Cminorgen.cmi 
 Coloring.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \
     Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
     ../caml/Coloringaux.cmi CList.cmi BinInt.cmi AST.cmi Coloring.cmi 
@@ -270,12 +282,6 @@ Coqlib.cmo: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \
     BinPos.cmi BinInt.cmi Coqlib.cmi 
 Coqlib.cmx: Zdiv.cmx ZArith_dec.cmx Wf.cmx Specif.cmx Datatypes.cmx CList.cmx \
     BinPos.cmx BinInt.cmx Coqlib.cmi 
-CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \
-    Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \
-    AST.cmi CSE.cmi 
-CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Kildall.cmx \
-    Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \
-    AST.cmx CSE.cmi 
 Csharpminor.cmo: Zmax.cmi Values.cmi Mem.cmi Maps.cmi Integers.cmi \
     Globalenvs.cmi Floats.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi \
     AST.cmi Csharpminor.cmi 
@@ -288,8 +294,6 @@ Cshmgen.cmo: Specif.cmi Peano.cmi Integers.cmi Floats.cmi Errors.cmi \
 Cshmgen.cmx: Specif.cmx Peano.cmx Integers.cmx Floats.cmx Errors.cmx \
     Datatypes.cmx Csyntax.cmx Csharpminor.cmx Cminor.cmx CString.cmx \
     CList.cmx Ascii.cmx AST.cmx Cshmgen.cmi 
-CString.cmo: Specif.cmi Datatypes.cmi Ascii.cmi CString.cmi 
-CString.cmx: Specif.cmx Datatypes.cmx Ascii.cmx CString.cmi 
 Csyntax.cmo: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Errors.cmi \
     Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi BinPos.cmi BinInt.cmi \
     Ascii.cmi AST.cmi Csyntax.cmi 
@@ -306,10 +310,6 @@ EqNat.cmo: Specif.cmi Datatypes.cmi EqNat.cmi
 EqNat.cmx: Specif.cmx Datatypes.cmx EqNat.cmi 
 Errors.cmo: Datatypes.cmi CString.cmi CList.cmi BinPos.cmi Errors.cmi 
 Errors.cmx: Datatypes.cmx CString.cmx CList.cmx BinPos.cmx Errors.cmi 
-Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \
-    Floats.cmi 
-Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \
-    Floats.cmi 
 FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi FSetList.cmi \
     Datatypes.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi 
 FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx FSetList.cmx \
@@ -324,6 +324,10 @@ FSetInterface.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx \
     FSetInterface.cmi 
 FSetList.cmo: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi FSetList.cmi 
 FSetList.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx FSetList.cmi 
+Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \
+    Floats.cmi 
+Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \
+    Floats.cmi 
 Globalenvs.cmo: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \
     CList.cmi BinPos.cmi BinInt.cmi AST.cmi Globalenvs.cmi 
 Globalenvs.cmx: Values.cmx Mem.cmx Maps.cmx Integers.cmx Datatypes.cmx \
@@ -348,10 +352,28 @@ Kildall.cmo: Specif.cmi Setoid.cmi OrderedType.cmi Ordered.cmi Maps.cmi \
 Kildall.cmx: Specif.cmx Setoid.cmx OrderedType.cmx Ordered.cmx Maps.cmx \
     Lattice.cmx Iteration.cmx FSetFacts.cmx FSetAVL.cmx Datatypes.cmx \
     Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx Kildall.cmi 
+LTL.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
+    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
+    BinPos.cmi BinInt.cmi AST.cmi LTL.cmi 
+LTL.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx Locations.cmx \
+    Integers.cmx Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.cmx \
+    BinPos.cmx BinInt.cmx AST.cmx LTL.cmi 
+LTLin.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi LTLin.cmi 
+LTLin.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
+    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
+    AST.cmx LTLin.cmi 
 Lattice.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \
     BinPos.cmi Lattice.cmi 
 Lattice.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Bool.cmx \
     BinPos.cmx Lattice.cmi 
+Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi Linear.cmi 
+Linear.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
+    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
+    AST.cmx Linear.cmi 
 Linearize.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \
     ../caml/Linearizeaux.cmo Lattice.cmi LTLin.cmi LTL.cmi Kildall.cmi \
     FSetAVL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi \
@@ -360,30 +382,12 @@ Linearize.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Op.cmx Maps.cmx \
     ../caml/Linearizeaux.cmx Lattice.cmx LTLin.cmx LTL.cmx Kildall.cmx \
     FSetAVL.cmx Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx \
     BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx Linearize.cmi 
-Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi Linear.cmi 
-Linear.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx Linear.cmi 
 Locations.cmo: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \
     BinInt.cmi AST.cmi Locations.cmi 
 Locations.cmx: Values.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \
     BinInt.cmx AST.cmx Locations.cmi 
 Logic.cmo: Logic.cmi 
 Logic.cmx: Logic.cmi 
-LTLin.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi LTLin.cmi 
-LTLin.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx LTLin.cmi 
-LTL.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Locations.cmi \
-    Integers.cmi Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi \
-    BinPos.cmi BinInt.cmi AST.cmi LTL.cmi 
-LTL.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Maps.cmx Locations.cmx \
-    Integers.cmx Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.cmx \
-    BinPos.cmx BinInt.cmx AST.cmx LTL.cmi 
 Mach.cmo: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Maps.cmi \
     Locations.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi \
     CList.cmi BinPos.cmi BinInt.cmi AST.cmi Mach.cmi 
@@ -416,6 +420,18 @@ Ordered.cmx: Specif.cmx OrderedType.cmx Maps.cmx Datatypes.cmx Coqlib.cmx \
     BinPos.cmx Ordered.cmi 
 OrderedType.cmo: Specif.cmi Datatypes.cmi OrderedType.cmi 
 OrderedType.cmx: Specif.cmx Datatypes.cmx OrderedType.cmi 
+PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi Globalenvs.cmi \
+    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
+    AST.cmi PPC.cmi 
+PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx Globalenvs.cmx \
+    Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
+    AST.cmx PPC.cmi 
+PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \
+    Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \
+    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi PPCgen.cmi 
+PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx Integers.cmx \
+    Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx Bool.cmx \
+    BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx PPCgen.cmi 
 Parallelmove.cmo: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi \
     Parallelmove.cmi 
 Parallelmove.cmx: Parmov.cmx Locations.cmx Datatypes.cmx CList.cmx AST.cmx \
@@ -424,28 +440,12 @@ Parmov.cmo: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi Parmov.cmi
 Parmov.cmx: Specif.cmx Peano.cmx Datatypes.cmx CList.cmx Parmov.cmi 
 Peano.cmo: Datatypes.cmi Peano.cmi 
 Peano.cmx: Datatypes.cmx Peano.cmi 
-PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \
-    Errors.cmi Datatypes.cmi Coqlib.cmi CString.cmi CList.cmi Bool.cmi \
-    BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi PPCgen.cmi 
-PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx Integers.cmx \
-    Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx Bool.cmx \
-    BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx PPCgen.cmi 
-PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi Globalenvs.cmi \
-    Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \
-    AST.cmi PPC.cmi 
-PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx Globalenvs.cmx \
-    Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \
-    AST.cmx PPC.cmi 
-Registers.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi FSetAVL.cmi \
-    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
-    Registers.cmi 
-Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \
-    Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
-    Registers.cmi 
-Reload.cmo: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
-    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi Reload.cmi 
-Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \
-    LTLin.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx Reload.cmi 
+RTL.cmo: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
+    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
+    RTL.cmi 
+RTL.cmx: Values.cmx Registers.cmx Op.cmx Mem.cmx Maps.cmx Integers.cmx \
+    Globalenvs.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
+    RTL.cmi 
 RTLgen.cmo: Switch.cmi Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi \
     Op.cmi Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
     CminorSel.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi \
@@ -454,12 +454,6 @@ RTLgen.cmx: Switch.cmx Specif.cmx Registers.cmx ../caml/RTLgenaux.cmx RTL.cmx \
     Op.cmx Maps.cmx Integers.cmx Errors.cmx Datatypes.cmx Coqlib.cmx \
     CminorSel.cmx CString.cmx CList.cmx BinPos.cmx Ascii.cmx AST.cmx \
     RTLgen.cmi 
-RTL.cmo: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \
-    Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
-    RTL.cmi 
-RTL.cmx: Values.cmx Registers.cmx Op.cmx Mem.cmx Maps.cmx Integers.cmx \
-    Globalenvs.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
-    RTL.cmi 
 RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \
     Op.cmi Maps.cmi Errors.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \
     CString.cmi CList.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi \
@@ -468,6 +462,16 @@ RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \
     Op.cmx Maps.cmx Errors.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \
     CString.cmx CList.cmx BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx \
     RTLtyping.cmi 
+Registers.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi FSetAVL.cmi \
+    Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
+    Registers.cmi 
+Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \
+    Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
+    Registers.cmi 
+Reload.cmo: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
+    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi Reload.cmi 
+Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \
+    LTLin.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx Reload.cmi 
 Selection.cmo: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \
     CminorSel.cmi Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \
     Selection.cmi 
diff --git a/test/c/Makefile b/test/c/Makefile
index 3f4ea40a..3ee10c94 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -9,10 +9,12 @@ LIBS=
 TIME=xtime -o /dev/null -mintime 1.0     # Xavier's hack
 #TIME=time >/dev/null                    # Otherwise
 
-PROGS=fib integr qsort fft sha1 aes almabench lists \
+BENCHS=fib integr qsort fft sha1 aes almabench lists \
   binarytrees fannkuch knucleotide mandelbrot nbody \
   nsieve nsievebits spectral
 
+PROGS=$(BENCHS) initializers
+
 all_s: $(PROGS:%=%.s)
 
 all: $(PROGS:%=%.compcert)
@@ -45,12 +47,12 @@ test_gcc:
          done
 
 time_gcc:
-	@for i in $(PROGS); do \
+	@for i in $(BENCHS); do \
 	   echo -n "$$i: "; $(TIME) ./$$i.gcc; \
          done
 
 time_compcert:
-	@for i in $(PROGS); do \
+	@for i in $(BENCHS); do \
 	   echo -n "$$i: "; $(TIME) ./$$i.compcert; \
          done
 
diff --git a/test/c/Results/initializers b/test/c/Results/initializers
new file mode 100644
index 00000000..67be47f4
--- /dev/null
+++ b/test/c/Results/initializers
diff --git a/test/c/initializers.c b/test/c/initializers.c
new file mode 100644
index 00000000..da45e5bb
--- /dev/null
+++ b/test/c/initializers.c
@@ -0,0 +1,48 @@
+#include <stdio.h>
+
+char x1 = 'x';
+
+int x2 = 12345;
+
+double x3 = 3.14159;
+
+char x4[4] = { 'a', 'b', 'c', 'd' };
+
+int x5[10] = { 1, 2, 3 };
+
+struct { int y; int z; } x6 = { 4, 5 };
+
+struct { int y; char z; } x7 = { 6, 'u' };
+
+struct { char y; int z; } x8 = { 'v', 7 };
+
+struct { char y[9]; double z; } x9 = { { 'a', 'b' }, 2.718 };
+
+struct {
+  struct { char y; int z; } u;
+  double v;
+} x10 = { { 'v', 7 }, 2.718 };
+
+int main(int argc, char ** argv)
+{
+  int i;
+
+  printf("x1 = '%c'\n", x1);
+  printf("x2 = %d\n", x2);
+  printf("x3 = %.5f\n", x3);
+  printf("x4 = { '%c', '%c', '%c', '%c' }\n",
+         x4[0], x4[1], x4[2], x4[3]);
+  printf("x5 = { ");
+  for (i = 0; i < 10; i++) printf("%d, ", x5[i]);
+  printf("}\n");
+  printf("x6 = { %d, %d }\n", x6.y, x6.z);
+  printf("x7 = { %d, '%c' }\n", x7.y, x7.z);
+  printf("x8 = { '%c', %d }\n", x8.y, x8.z);
+  printf("x9 = { { ");
+  for (i = 0; i < 9; i++) printf("'%c', ", x9.y[i]);
+  printf("}, %.3f }\n", x9.z);
+  printf("x10 = { { '%c', %d }, %.3f }\n",
+         x10.u.y, x10.u.z, x10.v);
+  return 0;
+}
+