diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-19 11:18:10 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-19 11:18:10 +0100 |
| commit | 253e8e9b72a1204f334460af0ffc7893d3e4b752 (patch) | |
| tree | aa1624235503658fe19e8d1658ae05db350cf32b /backend/PrintAsm.ml | |
| parent | f750e0ac9ee99072cca8361f591015f1f82681fa (diff) | |
| download | compcert-kvx-253e8e9b72a1204f334460af0ffc7893d3e4b752.tar.gz compcert-kvx-253e8e9b72a1204f334460af0ffc7893d3e4b752.zip | |
Activating the printing of the debug information for supported architecture.
Diffstat (limited to 'backend/PrintAsm.ml')
| -rw-r--r-- | backend/PrintAsm.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 510dbc64..05b55a10 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -88,6 +88,8 @@ 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 @@ -102,6 +104,8 @@ let print_program oc p db = PrintAnnot.close_filenames (); if !Clflags.option_g && Configuration.advanced_debug then begin - let module DebugPrinter = DwarfPrinter(Target) in - () + match db with + | None -> () + | Some db -> + Printer.DebugPrinter.print_debug oc db end |