aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-02-18 15:06:53 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-02-18 15:06:53 +0100
commitfcd5ba10674f499d4e270bfb68fa40da8857fb47 (patch)
treeec56ae5a6b28f85fa1670342cf26032f4ed26d6f /backend
parent71260eff997f5d3c25d9ccda92b8176c893be26d (diff)
downloadcompcert-kvx-fcd5ba10674f499d4e270bfb68fa40da8857fb47.tar.gz
compcert-kvx-fcd5ba10674f499d4e270bfb68fa40da8857fb47.zip
Added an elf prefix to all common elf functions in PrintAsmaux.
Diffstat (limited to 'backend')
-rw-r--r--backend/PrintAsm.ml8
-rw-r--r--backend/PrintAsmaux.ml24
2 files changed, 15 insertions, 17 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index fb03d96b..c356d7e5 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -37,9 +37,9 @@ module Printer(Target:TARGET) =
match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in
Target.print_align oc alignment;
if not (C2C.atom_is_static name) then
- fprintf oc " .globl %a\n" symbol name;
+ fprintf oc " .globl %a\n" Target.symbol name;
Target.print_optional_fun_info oc;
- fprintf oc "%a:\n" symbol name;
+ fprintf oc "%a:\n" Target.symbol name;
print_location oc (C2C.atom_location name);
Target.cfi_startproc oc;
Target.print_instructions oc fn;
@@ -74,8 +74,8 @@ module Printer(Target:TARGET) =
fprintf oc " %s\n" name_sec;
Target.print_align oc align;
if not (C2C.atom_is_static name) then
- fprintf oc " .global %a\n" symbol name;
- fprintf oc "%a:\n" symbol name;
+ fprintf oc " .global %a\n" Target.symbol name;
+ fprintf oc "%a:\n" Target.symbol name;
print_init_data oc name v.gvar_init;
Target.print_var_info oc name;
end else
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index f3d95f87..925add9e 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -41,6 +41,7 @@ module type TARGET =
val section: out_channel -> section_name -> unit
val name_of_section: section_name -> string
val comment: string
+ val symbol: out_channel -> P.t -> unit
end
(* On-the-fly label renaming *)
@@ -60,7 +61,7 @@ let transl_label lbl =
Hashtbl.add current_function_labels lbl lbl';
lbl'
-let label oc lbl =
+let elf_label oc lbl =
fprintf oc ".L%d" lbl
(* List of literals and jumptables used in the code *)
@@ -81,25 +82,22 @@ let current_function_sig =
ref { sig_args = []; sig_res = None; sig_cc = cc_default }
(* Functions for printing of symbol names *)
-let symbol oc symb =
+let elf_symbol oc symb =
fprintf oc "%s" (extern_atom symb)
-let symbol_offset oc (symb, ofs) =
- symbol oc symb;
+let elf_symbol_offset oc (symb, ofs) =
+ elf_symbol oc symb;
let ofs = camlint_of_coqint ofs in
if ofs <> 0l then fprintf oc " + %ld" ofs
-(* The comment deliminiter *)
-let comment = "#"
-
(* Functions for fun and var info *)
-let print_fun_info oc name =
- fprintf oc " .type %a, @function\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name
+let elf_print_fun_info oc name =
+ fprintf oc " .type %a, @function\n" elf_symbol name;
+ fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name
-let print_var_info oc name =
- fprintf oc " .type %a, @object\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name
+let elf_print_var_info oc name =
+ fprintf oc " .type %a, @object\n" elf_symbol name;
+ fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name
(* Emit .cfi directives *)
let cfi_startproc =