From ccddcdc4a8aecca88188e3355958f55d44c83400 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Mar 2010 08:45:53 +0000 Subject: Pretty strings git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/PrintAsm.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'arm') diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index b04d46ea..77bacc3c 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; -- cgit