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 /debug/Dwarfgen.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 'debug/Dwarfgen.ml')
| -rw-r--r-- | debug/Dwarfgen.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index de07add1..50063df8 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -344,7 +344,7 @@ module Dwarfgenaux (Target: TARGET) = let global_variable_to_entry acc id v = let loc = match v.gvar_atom with - | Some a when is_variable_printed (extern_atom a) -> + | Some a when is_symbol_printed (extern_atom a) -> Some (LocSymbol a) | _ -> None in let var = { @@ -529,7 +529,10 @@ module Dwarfgenaux (Target: TARGET) = match t with | GlobalVariable g -> Some (global_variable_to_entry acc id g) | Function f -> + if is_symbol_printed f.fun_name then Some (function_to_entry sec_name acc id f) + else + None end |