aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/PrintLinux.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-01-12 14:20:31 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-01-12 14:20:31 +0100
commit81e91f965e7b1afbea8d1630015e75f11f0a3afd (patch)
tree270a85299f33d783e33745c917796f080f7300e1 /powerpc/PrintLinux.ml
parent3304820b870e4524c7d1f14fcd62506634f7922b (diff)
parent06841a5bb7ca27bc436e87e7991d0d05dbf5267c (diff)
downloadcompcert-81e91f965e7b1afbea8d1630015e75f11f0a3afd.tar.gz
compcert-81e91f965e7b1afbea8d1630015e75f11f0a3afd.zip
Merge branch 'master' into dwarf
Conflicts: powerpc/PrintAsm.ml
Diffstat (limited to 'powerpc/PrintLinux.ml')
-rw-r--r--powerpc/PrintLinux.ml16
1 files changed, 2 insertions, 14 deletions
diff --git a/powerpc/PrintLinux.ml b/powerpc/PrintLinux.ml
index 4e90308c..7ed98d2e 100644
--- a/powerpc/PrintLinux.ml
+++ b/powerpc/PrintLinux.ml
@@ -68,21 +68,9 @@ module Linux_System =
sprintf ".section \"%s\",\"a%s%s\",@progbits"
s (if wr then "w" else "") (if ex then "x" else "")
- let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7
- let reset_file_line () = Hashtbl.clear filename_num
let print_file_line oc file line =
- if !Clflags.option_g && file <> "" then begin
- let filenum =
- try
- Hashtbl.find filename_num file
- with Not_found ->
- let n = Hashtbl.length filename_num + 1 in
- Hashtbl.add filename_num file n;
- fprintf oc " .file %d %S\n" n file;
- n
- in fprintf oc " .loc %d %s\n" filenum line
- end
-
+ PrintAnnot.print_file_line oc comment file line
+
(* Emit .cfi directives *)
let cfi_startproc =
if Configuration.asm_supports_cfi then