From fd04963da2f16cf22de5613bb793b0302ea99b70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 31 Oct 2007 17:09:12 +0000 Subject: 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/PrintPPC.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'caml/PrintPPC.ml') 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 -- cgit