diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-02 00:07:04 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-02 00:07:04 +0200 |
| commit | a0bef6920c64f2d0e51d4bdce2f08c927373fb66 (patch) | |
| tree | 9bdd722b483ca10c8f0d6249cd1af82d12f69f5c /debug/DwarfPrinter.ml | |
| parent | 2d96b7927719c3b61fe564e8ab273a1b154912a5 (diff) | |
| download | compcert-kvx-a0bef6920c64f2d0e51d4bdce2f08c927373fb66.tar.gz compcert-kvx-a0bef6920c64f2d0e51d4bdce2f08c927373fb66.zip | |
Started implementation of gnu compatible debug information.
Diffstat (limited to 'debug/DwarfPrinter.ml')
| -rw-r--r-- | debug/DwarfPrinter.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index d0410b93..79d21960 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -590,12 +590,15 @@ module DwarfPrinter(Target: DWARF_TARGET): let print_location_list oc (c_low,l) = List.iter (print_location_entry oc c_low) l - (* Print the debug info and abbrev section *) - let print_debug oc entries = + let print_diab_entries oc entries = print_debug_abbrev oc entries; List.iter (fun (s,d,e,_) -> print_debug_info oc s d e) entries; section oc Section_debug_loc; List.iter (fun (_,_,_,l) -> print_location_list oc l) entries + (* Print the debug info and abbrev section *) + let print_debug oc = function + | Diab entries -> print_diab_entries oc entries + | _ -> () end |