1 files changed, 37 insertions, 42 deletions

diff --git a/debug/Debug.mli b/debug/Debug.mli
index 577b0ef8..1585e7e4 100644
--- a/debug/Debug.mli
+++ b/debug/Debug.mli
@@ -15,54 +15,52 @@ open C
 open Camlcoq
 open DwarfTypes
 open BinNums
+open Sections
 
 
 (* Record used for stroring references to the actual implementation functions *)
-type implem = 
+type implem =
     {
-     mutable init: string -> unit;
-     mutable atom_function: ident -> atom -> unit;
-     mutable atom_global_variable: ident -> atom -> unit;
-     mutable set_composite_size: ident -> struct_or_union -> int option -> unit;
-     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 generate_debug_info: (atom -> string) -> string -> debug_entries option;
-     mutable all_files_iter: (string -> unit) -> unit;
-     mutable insert_local_declaration:  storage -> ident -> typ -> location -> unit;
-     mutable atom_local_variable: ident -> atom -> unit;
-     mutable enter_scope: int -> int -> int -> unit;
-     mutable enter_function_scope: int -> int -> unit;
-     mutable add_lvar_scope: int -> ident -> int -> unit;
-     mutable open_scope: atom -> int -> positive -> unit;
-     mutable close_scope: atom -> int -> positive -> unit;
-     mutable start_live_range: (atom * atom) -> positive -> int * int builtin_arg -> unit;
-     mutable end_live_range: (atom * atom) -> positive -> unit;
-     mutable stack_variable: (atom * atom) -> int * int builtin_arg -> unit;
-     mutable function_end: atom -> positive -> unit;
-     mutable add_label: atom -> positive -> int -> unit;
-     mutable atom_parameter: ident -> ident -> atom -> unit;
-     mutable add_compilation_section_start: string -> int -> unit;
-     mutable add_compilation_section_end: string -> int -> unit;
-     mutable compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit;
-     mutable compute_gnu_file_enum: (string -> unit) -> unit;
-     mutable exists_section: string -> bool;
-     mutable remove_unused: ident -> unit;
-     mutable variable_printed: string -> unit;
-     mutable add_diab_info: string -> (int * int * string) -> unit;
+     init: string -> unit;
+     atom_global: ident -> atom -> unit;
+     set_composite_size: ident -> struct_or_union -> int option -> unit;
+     set_member_offset: ident -> string -> int -> unit;
+     set_bitfield_offset: ident -> string -> int -> string -> int -> unit;
+     insert_global_declaration: Env.t -> globdecl -> unit;
+     add_fun_addr: atom -> section_name -> (int * int) -> unit;
+     generate_debug_info: (atom -> string) -> string -> debug_entries option;
+     all_files_iter: (string -> unit) -> unit;
+     insert_local_declaration:  storage -> ident -> typ -> location -> unit;
+     atom_local_variable: ident -> atom -> unit;
+     enter_scope: int -> int -> int -> unit;
+     enter_function_scope: int -> int -> unit;
+     add_lvar_scope: int -> ident -> int -> unit;
+     open_scope: atom -> int -> positive -> unit;
+     close_scope: atom -> int -> positive -> unit;
+     start_live_range: (atom * atom) -> positive -> int * int builtin_arg -> unit;
+     end_live_range: (atom * atom) -> positive -> unit;
+     stack_variable: (atom * atom) -> int * int builtin_arg -> unit;
+     add_label: atom -> positive -> int -> unit;
+     atom_parameter: ident -> ident -> atom -> unit;
+     compute_diab_file_enum: (section_name -> int) -> (string-> int) -> (unit -> unit) -> unit;
+     compute_gnu_file_enum: (string -> unit) -> unit;
+     exists_section: section_name -> bool;
+     remove_unused: ident -> unit;
+     variable_printed: string -> unit;
+     add_diab_info: section_name ->  int -> int -> int -> unit;
    }
 
-val implem: implem
+val default_implem: implem
+
+val implem: implem ref
 
 val init_compile_unit: string -> unit
-val atom_function: ident -> atom -> unit
-val atom_global_variable: ident -> atom -> unit
+val atom_global: ident -> atom -> unit
 val set_composite_size: ident -> struct_or_union -> int option -> unit
 val set_member_offset: ident -> string -> int -> unit
 val set_bitfield_offset: ident -> string -> int -> string -> int -> unit
 val insert_global_declaration:  Env.t -> globdecl -> unit
-val add_fun_addr: atom -> (int * int) -> unit
+val add_fun_addr: atom -> section_name -> (int * int) -> unit
 val all_files_iter: (string -> unit) -> unit
 val insert_local_declaration: storage -> ident -> typ -> location -> unit
 val atom_local_variable: ident -> atom -> unit
@@ -74,15 +72,12 @@ val close_scope: atom -> int -> positive -> unit
 val start_live_range: (atom * atom) -> positive -> (int * int builtin_arg) -> unit
 val end_live_range: (atom * atom) -> positive -> unit
 val stack_variable: (atom * atom) -> int * int builtin_arg -> unit
-val function_end: atom -> positive -> unit
 val add_label: atom -> positive -> int -> unit
 val generate_debug_info: (atom -> string) -> string -> debug_entries option
 val atom_parameter: ident -> ident -> atom -> unit
-val add_compilation_section_start: string -> int -> unit
-val add_compilation_section_end: string -> int -> unit
-val compute_diab_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit
+val compute_diab_file_enum: (section_name -> int) -> (string-> int) -> (unit -> unit) -> unit
 val compute_gnu_file_enum: (string -> unit) -> unit
-val exists_section: string -> bool
+val exists_section: section_name -> bool
 val remove_unused: ident -> unit
 val variable_printed: string -> unit
-val add_diab_info: string -> (int * int * string) -> unit
+val add_diab_info: section_name ->  int -> int  -> int -> unit