diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-04-09 18:16:09 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-04-16 18:33:35 +0200 |
| commit | 65ac4adf1fb1c2642a8e69d098049dfa2ab90e92 (patch) | |
| tree | b1a3c480ca621b8c7dfecb430507e5ca0e72e88b /debug | |
| parent | 5beeba02f16b2d65cceec5ee5577547ba3547c94 (diff) | |
| download | compcert-kvx-65ac4adf1fb1c2642a8e69d098049dfa2ab90e92.tar.gz compcert-kvx-65ac4adf1fb1c2642a8e69d098049dfa2ab90e92.zip | |
Simplified offset printing.
Instead of printing an the start label and adding the offset by
computing the difference of the range label and the start label
use the range label directly.
Bug 26234
Diffstat (limited to 'debug')
| -rw-r--r-- | debug/DwarfPrinter.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 5634d58c..c5df5637 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -244,6 +244,7 @@ module DwarfPrinter(Target: DWARF_TARGET): (* Mapping from abbreviation string to abbreviaton id *) let abbrev_mapping: (string,int) Hashtbl.t = Hashtbl.create 7 + (* Mapping from abbreviation range id to label *) let range_labels : (int, int) Hashtbl.t = Hashtbl.create 7 (* Look up the id of the abbreviation and add it if it is missing *) @@ -444,8 +445,8 @@ module DwarfPrinter(Target: DWARF_TARGET): | Offset i -> let lbl = new_label () in Hashtbl.add range_labels i lbl; - fprintf oc " .4byte %a+(%a-%a)%a\n" - label !debug_ranges_addr label lbl label !debug_ranges_addr print_comment "DW_AT_ranges" + fprintf oc " .4byte %a%a\n" + label lbl print_comment "DW_AT_ranges" | _ -> () let print_compilation_unit oc tag = |