diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-04 22:15:20 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-04 22:15:20 +0200 |
| commit | 34cc6a603f34a430fc3b9a7071dcc1e19b2b7250 (patch) | |
| tree | 2bc811f0893b7925164f70e0b284ea6061aca36c /backend/Fileinfo.ml | |
| parent | 57fceab9ba11cb98635236f31c85ca976ca7f48c (diff) | |
| download | compcert-kvx-34cc6a603f34a430fc3b9a7071dcc1e19b2b7250.tar.gz compcert-kvx-34cc6a603f34a430fc3b9a7071dcc1e19b2b7250.zip | |
Ensure that there are file directives for all files used in the debug
information.
Diffstat (limited to 'backend/Fileinfo.ml')
| -rw-r--r-- | backend/Fileinfo.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/backend/Fileinfo.ml b/backend/Fileinfo.ml index afdea382..0490def0 100644 --- a/backend/Fileinfo.ml +++ b/backend/Fileinfo.ml @@ -42,16 +42,17 @@ let enter_filename f = (* Add file and line debug location, using GNU assembler-style DWARF2 directives *) +let print_file oc file = + try + Hashtbl.find filename_info file + with Not_found -> + let (filenum, filebuf as res) = enter_filename file in + fprintf oc " .file %d %S\n" filenum file; + res let print_file_line oc pref file line = if !Clflags.option_g && file <> "" then begin - let (filenum, filebuf) = - try - Hashtbl.find filename_info file - with Not_found -> - let (filenum, filebuf as res) = enter_filename file in - fprintf oc " .file %d %S\n" filenum file; - res in + let (filenum, filebuf) = print_file oc file in fprintf oc " .loc %d %d\n" filenum line; match filebuf with | None -> () |