diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-06 20:32:55 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-06 20:32:55 +0200 |
commit | 861292a6c5e58b4f78bef207c717b801b3fc1fed (patch) | |
tree | 970be0db2fb62e66b09c4fb90b2e750c255565e0 /backend | |
parent | dba05a9f6259c82a350987b511bf1a71f113d0ba (diff) | |
download | compcert-kvx-861292a6c5e58b4f78bef207c717b801b3fc1fed.tar.gz compcert-kvx-861292a6c5e58b4f78bef207c717b801b3fc1fed.zip |
Startet implementation of new Debug interface.
Added a new file debug/Debug.ml which will be the interface between for
generating and printing the debuging information. Currently it contains
only the code for the line directived.
Diffstat (limited to 'backend')
-rw-r--r-- | backend/PrintAsm.ml | 4 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 71 |
2 files changed, 2 insertions, 73 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 29409b32..b88a3d50 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -134,12 +134,12 @@ module Printer(Target:TARGET) = let print_program oc p db = let module Target = (val (sel_target ()):TARGET) in let module Printer = Printer(Target) in - reset_filenames (); + Debug.reset_filenames (); print_version_and_options oc Target.comment; Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; - close_filenames (); + Debug.close_filenames (); if !Clflags.option_g && Configuration.advanced_debug then begin match db with diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 324e7e66..441f8251 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -142,77 +142,6 @@ let cfi_rel_offset = let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) -(* Printing annotations in asm syntax *) -(** All files used in the debug entries *) -module StringSet = Set.Make(String) -let all_files : StringSet.t ref = ref StringSet.empty -let add_file file = - all_files := StringSet.add file !all_files - - -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 DWARF2 directives in the style - of Diab C 5 *) - -let print_file_line_d2 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 " .d2file %S\n" file; - last_file := file - end; - fprintf oc " .d2line %d\n" line; - match filebuf with - | None -> () - | Some fb -> Printlines.copy oc pref fb line line - end - (** Programmer-supplied annotations (__builtin_annot). *) let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" |