diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-01 12:19:16 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-01 12:19:16 +0200 |
| commit | eaf4bab84af4b3db1ca9c6785ed803bbbd61b9a7 (patch) | |
| tree | f6233fc2272d6495ec22afafd5ef5534ba32df44 /debug/DebugInformation.ml | |
| parent | 06a1a35d759dc780e389218b5f78ce3415d4b3cd (diff) | |
| download | compcert-kvx-eaf4bab84af4b3db1ca9c6785ed803bbbd61b9a7.tar.gz compcert-kvx-eaf4bab84af4b3db1ca9c6785ed803bbbd61b9a7.zip | |
Only print locations for symbols that are present in the assembler.
Diffstat (limited to 'debug/DebugInformation.ml')
| -rw-r--r-- | debug/DebugInformation.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index b14548e7..654c983c 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -810,6 +810,11 @@ let compute_file_enum end_label entry_label line_end = Hashtbl.add filenum (sec,file) lbl) !all_files; line_end ()) compilation_section_start +let printed_vars: StringSet.t ref = ref StringSet.empty + +let variable_printed id = + printed_vars := StringSet.add id !printed_vars + let init name = id := 0; file_name := name; @@ -826,4 +831,5 @@ let init name = Hashtbl.reset compilation_section_start; Hashtbl.reset compilation_section_end; Hashtbl.reset filenum; - all_files := StringSet.empty + all_files := StringSet.empty; + printed_vars := StringSet.empty; |