aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-12-07 10:10:33 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-12-07 10:10:33 +0100
commit680444f180c750078a77b0591cd5c19e632612d6 (patch)
tree18b006bd2ea8e8c0d2ab4cb34f96afffc9621d11 /debug
parent9683212947ec3e4efe431efe589897c34f999d15 (diff)
downloadcompcert-kvx-680444f180c750078a77b0591cd5c19e632612d6.tar.gz
compcert-kvx-680444f180c750078a77b0591cd5c19e632612d6.zip
More verbose dwarf.
Diffstat (limited to 'debug')
-rw-r--r--debug/DwarfPrinter.ml4
-rw-r--r--debug/DwarfTypes.mli2
-rw-r--r--debug/Dwarfgen.ml4
3 files changed, 6 insertions, 4 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index c9eb5acc..b81507a8 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -308,7 +308,9 @@ module DwarfPrinter(Target: DWARF_TARGET):
let print_string oc c = function
| Simple_string s ->
fprintf oc " .asciz \"%s\"%a\n" s print_comment c
- | Offset_string o -> print_loc_ref oc c o
+ | Offset_string (o,s) ->
+ let c = sprintf "%s %s" c s in
+ print_loc_ref oc c o
let print_uleb128 oc c d =
fprintf oc " .uleb128 %d%a\n" d print_comment c
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 566fa16c..48da4509 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -57,7 +57,7 @@ type bound_value =
type string_const =
| Simple_string of string
- | Offset_string of reference
+ | Offset_string of reference * string
type file_loc =
| Diab_file_loc of constant * constant
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index 65cd4951..30e44e52 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -583,11 +583,11 @@ let gnu_string_entry s =
Simple_string s
else
try
- Offset_string (Hashtbl.find string_table s)
+ Offset_string ((Hashtbl.find string_table s),s)
with Not_found ->
let id = next_id () in
Hashtbl.add string_table s id;
- Offset_string id
+ Offset_string (id,s)
let gen_gnu_debug_info sec_name var_section : debug_entries =