diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-04-08 17:24:28 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-04-16 18:33:35 +0200 |
| commit | 5beeba02f16b2d65cceec5ee5577547ba3547c94 (patch) | |
| tree | d2b4a85eb75f06f963648fc995ee9977dfd35f98 /backend/PrintAsm.ml | |
| parent | 06d846bd517cb0e47ab7b55cdbc912939524ca26 (diff) | |
| download | compcert-kvx-5beeba02f16b2d65cceec5ee5577547ba3547c94.tar.gz compcert-kvx-5beeba02f16b2d65cceec5ee5577547ba3547c94.zip | |
Print only debug info for printed functions.
Functions that are removed from the compilation unit, for example
inline functions without extern, should not produce debug
information.
This commit reuses the mechanism used for variables in order to
track additionally the printed functions. Therefore the printed
variable versions are exchanged for a printed symbol version.
Bug 26234
Diffstat (limited to 'backend/PrintAsm.ml')
| -rw-r--r-- | backend/PrintAsm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 92d465d5..dd428808 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -40,6 +40,7 @@ module Printer(Target:TARGET) = let print_function oc name fn = Hashtbl.clear current_function_labels; + Debug.symbol_printed (extern_atom name); let (text, lit, jmptbl) = Target.get_section_names name in Target.section oc text; let alignment = @@ -117,7 +118,7 @@ module Printer(Target:TARGET) = match v.gvar_init with | [] -> () | _ -> - Debug.variable_printed (extern_atom name); + Debug.symbol_printed (extern_atom name); let sec = match C2C.atom_sections name with | [s] -> s |