aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-01-07 13:53:20 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2015-01-07 13:53:20 +0100
commit06841a5bb7ca27bc436e87e7991d0d05dbf5267c (patch)
tree4bc44c26244008e2f424bf96ecc80ed58fb1b5e3 /backend
parent05f1cccccad587234c526225aa04aff041490051 (diff)
downloadcompcert-06841a5bb7ca27bc436e87e7991d0d05dbf5267c.tar.gz
compcert-06841a5bb7ca27bc436e87e7991d0d05dbf5267c.zip
In -g -S mode, annotate the generated asm file with the C source code in comments.
Refactor printing of .loc debug directives in backend/PrintAnnot.ml
Diffstat (limited to 'backend')
-rw-r--r--backend/PrintAnnot.ml67
1 files changed, 67 insertions, 0 deletions
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
index d24635a6..54174b9f 100644
--- a/backend/PrintAnnot.ml
+++ b/backend/PrintAnnot.ml
@@ -21,6 +21,73 @@ open AST
open Memdata
open Asm
+(** Line number annotations *)
+
+let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
+ = Hashtbl.create 7
+
+let last_file = ref ""
+
+let reset_filenames () =
+ Hashtbl.clear filename_info; last_file := ""
+
+let close_filenames () =
+ Hashtbl.iter
+ (fun file (num, fb) ->
+ match fb with Some b -> Printlines.close b | None -> ())
+ filename_info;
+ reset_filenames()
+
+let enter_filename f =
+ let num = Hashtbl.length filename_info + 1 in
+ let filebuf =
+ if !Clflags.option_S || !Clflags.option_dasm then begin
+ try Some (Printlines.openfile f)
+ with Sys_error _ -> None
+ end else None in
+ Hashtbl.add filename_info f (num, filebuf);
+ (num, filebuf)
+
+(* Add file and line debug location, using GNU assembler-style DWARF2
+ directives *)
+
+let print_file_line oc pref file line =
+ if !Clflags.option_g && file <> "" then begin
+ let (filenum, filebuf) =
+ try
+ Hashtbl.find filename_info file
+ with Not_found ->
+ let (filenum, filebuf as res) = enter_filename file in
+ fprintf oc " .file %d %S\n" filenum file;
+ res in
+ fprintf oc " .loc %d %d\n" filenum line;
+ match filebuf with
+ | None -> ()
+ | Some fb -> Printlines.copy oc pref fb line line
+ end
+
+(* Add file and line debug location, using DWARF1 directives in the style
+ of Diab C 5 *)
+
+let print_file_line_d1 oc pref file line =
+ if !Clflags.option_g && file <> "" then begin
+ let (_, filebuf) =
+ try
+ Hashtbl.find filename_info file
+ with Not_found ->
+ enter_filename file in
+ if file <> !last_file then begin
+ fprintf oc " .d1file %S\n" file;
+ last_file := file
+ end;
+ fprintf oc " .d1line %d\n" line;
+ match filebuf with
+ | None -> ()
+ | Some fb -> Printlines.copy oc pref fb line line
+ end
+
+(** "True" annotations *)
+
let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
type arg_value =