diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/PrintAnnot.ml | 8 | ||||
| -rw-r--r-- | backend/PrintAsm.ml | 14 | ||||
| -rw-r--r-- | backend/PrintAsm.mli | 4 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 8 |
4 files changed, 25 insertions, 9 deletions
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index 54174b9f..26f96370 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -66,10 +66,10 @@ let print_file_line oc pref file line = | Some fb -> Printlines.copy oc pref fb line line end -(* Add file and line debug location, using DWARF1 directives in the style +(* Add file and line debug location, using DWARF2 directives in the style of Diab C 5 *) -let print_file_line_d1 oc pref file line = +let print_file_line_d2 oc pref file line = if !Clflags.option_g && file <> "" then begin let (_, filebuf) = try @@ -77,10 +77,10 @@ let print_file_line_d1 oc pref file line = with Not_found -> enter_filename file in if file <> !last_file then begin - fprintf oc " .d1file %S\n" file; + fprintf oc " .d2file %S\n" file; last_file := file end; - fprintf oc " .d1line %d\n" line; + fprintf oc " .d2line %d\n" line; match filebuf with | None -> () | Some fb -> Printlines.copy oc pref fb line line diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index a6883339..05b55a10 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -15,6 +15,7 @@ open AST open Asm open Camlcoq open Datatypes +open DwarfPrinter open PrintAsmaux open Printf open Sections @@ -87,10 +88,12 @@ module Printer(Target:TARGET) = | Gfun (Internal code) -> print_function oc name code | Gfun (External ef) -> () | Gvar v -> print_var oc name v + + module DebugPrinter = DwarfPrinter (Target) end -let print_program oc p = +let print_program oc p db = let module Target = (val (sel_target ()):TARGET) in let module Printer = Printer(Target) in PrintAnnot.reset_filenames (); @@ -98,4 +101,11 @@ let print_program oc p = Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; - PrintAnnot.close_filenames () + PrintAnnot.close_filenames (); + if !Clflags.option_g && Configuration.advanced_debug then + begin + match db with + | None -> () + | Some db -> + Printer.DebugPrinter.print_debug oc db + end diff --git a/backend/PrintAsm.mli b/backend/PrintAsm.mli index eb63f1be..0b2869b0 100644 --- a/backend/PrintAsm.mli +++ b/backend/PrintAsm.mli @@ -11,6 +11,4 @@ (* *) (* *********************************************************************) -open PrintAsmaux - -val print_program: out_channel -> Asm.program -> unit +val print_program: out_channel -> Asm.program -> DwarfTypes.dw_entry option -> unit diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 64db2cb0..8bc961ef 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -14,6 +14,7 @@ open AST open Asm open Camlcoq +open DwarfTypes open Datatypes open Printf open Sections @@ -43,6 +44,13 @@ module type TARGET = val comment: string val symbol: out_channel -> P.t -> unit val default_falignment: int + val get_start_addr: unit -> int + val get_end_addr: unit -> int + val get_stmt_list_addr: unit -> int + val new_label: unit -> int + val label: out_channel -> int -> unit + val print_file_loc: out_channel -> file_loc -> unit + module DwarfAbbrevs: DWARF_ABBREVS end (* On-the-fly label renaming *) |