Skip to content
Snippets Groups Projects
Commit ccddcdc4 authored by xleroy's avatar xleroy
Browse files

Pretty strings

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 939d3eff
No related branches found
No related tags found
No related merge requests found
...@@ -543,8 +543,13 @@ let print_init oc = function ...@@ -543,8 +543,13 @@ let print_init oc = function
| Init_addrof(symb, ofs) -> | Init_addrof(symb, ofs) ->
fprintf oc " .word %a\n" print_symb_ofs (symb, ofs) fprintf oc " .word %a\n" print_symb_ofs (symb, ofs)
let print_init_data oc id = let print_init_data oc name id =
List.iter (print_init oc) 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), _)) = let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
match init_data with match init_data with
...@@ -555,7 +560,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = ...@@ -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 " .global %a\n" print_symb name;
fprintf oc " .type %a, %%object\n" print_symb name; fprintf oc " .type %a, %%object\n" print_symb name;
fprintf oc "%a:\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 = let print_program oc p =
extfuns := IdentSet.empty; extfuns := IdentSet.empty;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment