aboutsummaryrefslogtreecommitdiffstats
path: root/debug/Debug.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2019-04-08 17:24:28 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2019-04-16 18:33:35 +0200
commit5beeba02f16b2d65cceec5ee5577547ba3547c94 (patch)
treed2b4a85eb75f06f963648fc995ee9977dfd35f98 /debug/Debug.ml
parent06d846bd517cb0e47ab7b55cdbc912939524ca26 (diff)
downloadcompcert-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.ml')
-rw-r--r--debug/Debug.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/debug/Debug.ml b/debug/Debug.ml
index 168df5a0..812f57cc 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -47,7 +47,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;
}
@@ -79,7 +79,7 @@ let default_implem =
exists_section = (fun _ -> true);
remove_unused = (fun _ -> ());
remove_unused_function = (fun _ -> ());
- variable_printed = (fun _ -> ());
+ symbol_printed = (fun _ -> ());
add_diab_info = (fun _ _ _ _ -> ());
}
@@ -111,5 +111,5 @@ let compute_diab_file_enum end_l entry_l line_e = !implem.compute_diab_file_enum
let compute_gnu_file_enum f = !implem.compute_gnu_file_enum f
let remove_unused ident = !implem.remove_unused ident
let remove_unused_function ident = !implem.remove_unused_function ident
-let variable_printed ident = !implem.variable_printed ident
+let symbol_printed ident = !implem.symbol_printed ident
let add_diab_info sec line_start debug_info low_pc = !implem.add_diab_info sec line_start debug_info low_pc