diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-29 08:45:53 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-29 08:45:53 +0000 |
| commit | ccddcdc4a8aecca88188e3355958f55d44c83400 (patch) | |
| tree | f2aecaa118446f0449fc13aa67f2258dcf9879d2 | |
| parent | 939d3effd3f63e5a51d6bf0a6cf36e6ab82aac70 (diff) | |
Pretty strings
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
| -rw-r--r-- | arm/PrintAsm.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index b04d46e..77bacc3 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -543,8 +543,13 @@ let print_init oc = function | Init_addrof(symb, ofs) -> fprintf oc " .word %a\n" print_symb_ofs (symb, ofs) -let print_init_data oc id = - List.iter (print_init oc) id +let print_init_data oc name id = + if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 + && List.for_all (function Init_int8 _ -> true | _ -> false) id + then + fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id) + else + List.iter (print_init oc) id let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = match init_data with @@ -555,7 +560,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = fprintf oc " .global %a\n" print_symb name; fprintf oc " .type %a, %%object\n" print_symb name; fprintf oc "%a:\n" print_symb name; - print_init_data oc init_data + print_init_data oc name init_data let print_program oc p = extfuns := IdentSet.empty; |