From fd04963da2f16cf22de5613bb793b0302ea99b70 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 31 Oct 2007 17:09:12 +0000
Subject: [PATCH] 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
---
caml/Cil2Csyntax.ml | 105 ++++++++++-------
caml/PrintCsyntax.ml | 2 +-
caml/PrintPPC.ml | 9 +-
extraction/.depend | 228 ++++++++++++++++++------------------
test/c/Makefile | 8 +-
test/c/Results/initializers | Bin 0 -> 239 bytes
test/c/initializers.c | 48 ++++++++
7 files changed, 234 insertions(+), 166 deletions(-)
create mode 100644 test/c/Results/initializers
create mode 100644 test/c/initializers.c
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index 0e168414d..fd3ad4969 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 59c42d3bf..4eff1c686 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 bf7b2cc74..97082b9b6 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 60534fddf..62ab7b62c 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 3f4ea40ae..3ee10c94c 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 0000000000000000000000000000000000000000..67be47f4974dbd7d9086cf61d4a1c31b1cb27ac8
GIT binary patch
literal 239
zcmaKm%?iRm41_)JQ_L-wP@4Vewg(@^>MJM#>ARc677;{Ph76PaCMr0Cl#*r}B$wKf
z78}bTRoarYnt6gQ#GuvX>T)A&Nn2#X$c(}me?429Vy!Zof9l~TgWLl$zY89Q?Vc~;
Xzba2&`Byf(VdyeDK*ocxGe6l2+=?&g
literal 0
HcmV?d00001
diff --git a/test/c/initializers.c b/test/c/initializers.c
new file mode 100644
index 000000000..da45e5bb4
--- /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;
+}
+
--
GitLab