diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-04 22:17:45 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-04 22:17:45 +0200 |
commit | 8df444cbc4aa78d4effb03474b3709925ac7002a (patch) | |
tree | e251cf6733b0cf38ee125d649331687b829fe67a /backend | |
parent | 1b989dc9bff4a6425a929a5638362ca87edb122d (diff) | |
parent | 5493186b185143b8cea401fbbbf417d37ae7e665 (diff) | |
download | compcert-8df444cbc4aa78d4effb03474b3709925ac7002a.tar.gz compcert-8df444cbc4aa78d4effb03474b3709925ac7002a.zip |
Merge branch 'master' of github.com:AbsInt/CompCert
Diffstat (limited to 'backend')
-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 -> () |