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 | |
| 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.
| -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 = |