diff options
Diffstat (limited to 'backend/PrintAsm.ml')
| -rw-r--r-- | backend/PrintAsm.ml | 14 |
1 files changed, 12 insertions, 2 deletions
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 |