First version with computation of dwarf info from debug info.

Introduced a new dwarf generation from the information collected in
the DebugInformation and removed the old CtODwarf translation.

1 files changed, 15 insertions, 3 deletions

diff --git a/debug/Debug.ml b/debug/Debug.ml
index ab20f630..c45fd074 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -12,6 +12,8 @@
 
 open C
 open Camlcoq
+open Dwarfgen
+open DwarfTypes
 
 (* Interface for generating and printing debug information *)
 
@@ -25,7 +27,9 @@ type implem =
      mutable set_member_offset: ident -> string -> int -> unit;
      mutable set_bitfield_offset: ident -> string -> int -> string -> int -> unit;
      mutable insert_global_declaration: Env.t -> globdecl -> unit;
-     mutable add_fun_addr: atom -> (int * int) -> unit
+     mutable add_fun_addr: atom -> (int * int) -> unit;
+     mutable generate_debug_info: unit -> dw_entry option;
+     mutable all_files_iter: (string -> unit) -> unit;
    }
 
 let implem =
@@ -38,7 +42,9 @@ let implem =
    set_bitfield_offset = (fun _ _ _ _ _ -> ());
    insert_global_declaration = (fun _ _ -> ());
    add_fun_addr = (fun _ _ -> ());
- }
+   generate_debug_info = (fun _ -> None);
+   all_files_iter = (fun _ -> ());
+}
 
 let init () =
   if !Clflags.option_g then begin
@@ -50,6 +56,8 @@ let init () =
     implem.set_bitfield_offset <- DebugInformation.set_bitfield_offset;
     implem.insert_global_declaration <- DebugInformation.insert_global_declaration;
     implem.add_fun_addr <- DebugInformation.add_fun_addr;
+    implem.generate_debug_info <- (fun () -> Some (Dwarfgen.gen_debug_info ()));
+    implem.all_files_iter <- (fun f -> DebugInformation.StringSet.iter f !DebugInformation.all_files);
   end else begin
     implem.init <- (fun _ -> ());
     implem.atom_function <- (fun _ _ -> ());
@@ -58,7 +66,9 @@ let init () =
     implem.set_member_offset <- (fun _ _ _ -> ());
     implem.set_bitfield_offset <- (fun _ _ _ _ _ -> ());
     implem.insert_global_declaration <- (fun _ _ -> ());
-    implem.add_fun_addr <- (fun _ _ -> ())
+    implem.add_fun_addr <- (fun _ _ -> ());
+    implem.generate_debug_info <- (fun _ -> None);
+    implem.all_files_iter <- (fun _ -> ());
   end
 
 let init_compile_unit name = implem.init name
@@ -69,3 +79,5 @@ let set_member_offset id field off = implem.set_member_offset id field off
 let set_bitfield_offset id field off underlying size = implem.set_bitfield_offset id field off underlying size
 let insert_global_declaration env dec = implem.insert_global_declaration env dec
 let add_fun_addr atom addr = implem.add_fun_addr atom addr
+let generate_debug_info () = implem.generate_debug_info ()
+let all_files_iter f = implem.all_files_iter f