aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintAsm.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-28 18:39:43 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-28 18:39:43 +0200
commit68ad5472a78d12e0e4fd4eae422122185403d678 (patch)
tree52674e67c21c4134118996f2b241f9496f7f5130 /backend/PrintAsm.ml
parent5492b5b55afa68e3d628da07ff583a0cac79b7e3 (diff)
downloadcompcert-kvx-68ad5472a78d12e0e4fd4eae422122185403d678.tar.gz
compcert-kvx-68ad5472a78d12e0e4fd4eae422122185403d678.zip
Change the way the debug sections are printed.
If a user uses the #pragma use_section for functions the diab linker requires a separate debug_info section for each entry. This commit adds functionality to emulate this behavior.
Diffstat (limited to 'backend/PrintAsm.ml')
-rw-r--r--backend/PrintAsm.ml21
1 files changed, 11 insertions, 10 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 59570957..a152e3c2 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -24,8 +24,6 @@ open TargetPrinter
module Printer(Target:TARGET) =
struct
- let addr_mapping: (string, (int * int)) Hashtbl.t = Hashtbl.create 7
-
let get_fun_addr name =
let s = Target.new_label ()
and e = Target.new_label () in
@@ -38,7 +36,6 @@ module Printer(Target:TARGET) =
else
()
-
let print_location oc loc =
if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
@@ -113,11 +110,8 @@ module Printer(Target:TARGET) =
module DwarfTarget: DwarfTypes.DWARF_TARGET =
struct
let label = Target.label
- let name_of_section = Target.name_of_section
+ let section = Target.section
let print_file_loc = Target.print_file_loc
- let get_start_addr = Target.get_start_addr
- let get_end_addr = Target.get_end_addr
- let get_stmt_list_addr = Target.get_stmt_list_addr
let name_of_section = Target.name_of_section
let symbol = Target.symbol
end
@@ -136,8 +130,15 @@ let print_program oc p db =
close_filenames ();
if !Clflags.option_g && Configuration.advanced_debug then
begin
- match Debug.generate_debug_info () with
+ let atom_to_s s =
+ let s = C2C.atom_sections s in
+ match s with
+ | [] -> Target.name_of_section Section_text
+ | (Section_user (n,_,_))::_ -> n
+ | a::_ ->
+ Target.name_of_section a in
+ match Debug.generate_debug_info atom_to_s (Target.name_of_section Section_text) with
| None -> ()
- | Some (db,loc) ->
- Printer.DebugPrinter.print_debug oc db loc
+ | Some db ->
+ Printer.DebugPrinter.print_debug oc db
end