diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-31 17:09:12 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-31 17:09:12 +0000 |
| commit | fd04963da2f16cf22de5613bb793b0302ea99b70 (patch) | |
| tree | ca8bd1f4a56b9177c59ca837481d6564a8328ef1 /caml/PrintPPC.ml | |
| parent | 108804d88e16b00f171c2ac546c6c1a60f3c3ff8 (diff) | |
| download | compcert-fd04963da2f16cf22de5613bb793b0302ea99b70.tar.gz compcert-fd04963da2f16cf22de5613bb793b0302ea99b70.zip | |
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
Diffstat (limited to 'caml/PrintPPC.ml')
| -rw-r--r-- | caml/PrintPPC.ml | 9 |
1 files changed, 3 insertions, 6 deletions
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 |