diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-07-14 13:11:03 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-07-14 13:11:03 +0200 |
| commit | 2a78e5fd2f2c70fdd20048b3e23162ad97b2b2b6 (patch) | |
| tree | da5f5ddcff874828df008a02a1ec7e40c7d60244 /debug | |
| parent | b75e44331c506bfc51bc9283f686c116ac85f60d (diff) | |
| download | compcert-kvx-2a78e5fd2f2c70fdd20048b3e23162ad97b2b2b6.tar.gz compcert-kvx-2a78e5fd2f2c70fdd20048b3e23162ad97b2b2b6.zip | |
No verbose debug info in default mode.
We don't need verbose debug for the assembler. The verbose debug
information should only be printed if assembler files are
generated.
Diffstat (limited to 'debug')
| -rw-r--r-- | debug/DwarfPrinter.ml | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index bfd43b0b..09694d0b 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -27,11 +27,23 @@ module DwarfPrinter(Target: DWARF_TARGET): open Target - let print_comment oc s = - if s <> "" then - fprintf oc " %s %s" comment s - - let string_of_comment s = sprintf " %s %s" comment s + (* Do we need verbose debug information? *) + let include_comment = !Clflags.option_S || !Clflags.option_dasm + + (* Print comments needed for verbose debug mode *) + let print_comment = + if include_comment then + (fun oc s -> + if s <> "" then + fprintf oc " %s %s" comment s) + else + (fun _ _ -> ()) + + let string_of_comment = + if include_comment then + (fun s -> String.concat " " ["";comment;s]) + else + (fun _ -> "") (* Byte value to string *) let string_of_byte value ct = |