diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-06 11:08:58 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-06 11:08:58 +0200 |
| commit | 55eb2d92376f592258855cfa5c0cfbbf39e8e833 (patch) | |
| tree | 33ef79b3c21e3737202469cc6fb0bda064dd1146 /debug/DwarfPrinter.ml | |
| parent | 7c8693320818d00b26b4c36c2a01a5fe67c0c71b (diff) | |
| download | compcert-kvx-55eb2d92376f592258855cfa5c0cfbbf39e8e833.tar.gz compcert-kvx-55eb2d92376f592258855cfa5c0cfbbf39e8e833.zip | |
Fast fix for functions in different sections in one compilation unit for gcc.
Diffstat (limited to 'debug/DwarfPrinter.ml')
| -rw-r--r-- | debug/DwarfPrinter.ml | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 980c49db..2a54fa6a 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -590,8 +590,21 @@ module DwarfPrinter(Target: DWARF_TARGET): fprintf oc " .4byte 0\n"; fprintf oc " .4byte 0\n" + let print_location_entry_abs oc l = + print_label oc (loc_to_label l.loc_id); + List.iter (fun (b,e,loc) -> + fprintf oc " .4byte %a\n" label b; + fprintf oc " .4byte %a\n" label e; + print_list_loc oc loc) l.loc; + fprintf oc " .4byte 0\n"; + fprintf oc " .4byte 0\n" + + let print_location_list oc (c_low,l) = - List.iter (print_location_entry oc c_low) l + let f = match c_low with + | Some s -> print_location_entry oc s + | None -> print_location_entry_abs oc in + List.iter f l let print_diab_entries oc entries = let abbrev_start = new_label () in |