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/Debug.mli | |
| 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/Debug.mli')
| -rw-r--r-- | debug/Debug.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/debug/Debug.mli b/debug/Debug.mli index 3869a056..60e2f9bc 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -46,7 +46,7 @@ type implem = exists_section: section_name -> bool; remove_unused: ident -> unit; remove_unused_function: ident -> unit; - variable_printed: string -> unit; + symbol_printed: string -> unit; add_diab_info: section_name -> int -> int -> int -> unit; } @@ -80,5 +80,5 @@ val compute_gnu_file_enum: (string -> unit) -> unit val exists_section: section_name -> bool val remove_unused: ident -> unit val remove_unused_function: ident -> unit -val variable_printed: string -> unit +val symbol_printed: string -> unit val add_diab_info: section_name -> int -> int -> int -> unit |