Simplified DebugInformation interface.

Instead of exporting and setting all functions we just fill the
struct already in DebugInformation with the correct functions.

3 files changed, 36 insertions, 83 deletions

diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 6f159743..e3f5d98e 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -14,6 +14,7 @@ open BinNums
 open C
 open Camlcoq
 open Cutil
+open Debug
 open DebugTypes
 open Sections
 
@@ -660,3 +661,35 @@ let init name =
   Hashtbl.reset label_translation;
   all_files := StringSet.singleton name;
   printed_vars := StringSet.empty
+
+let default_debug =
+  {
+   init = init;
+   atom_global = atom_global;
+   set_composite_size = set_composite_size;
+   set_member_offset = set_member_offset;
+   set_bitfield_offset = set_bitfield_offset;
+   insert_global_declaration = insert_global_declaration;
+   add_fun_addr = (fun _ _ _ -> ());
+   generate_debug_info = (fun _ _  -> None);
+   all_files_iter = all_files_iter;
+   insert_local_declaration = insert_local_declaration;
+   atom_local_variable = atom_local_variable;
+   enter_scope = enter_scope;
+   enter_function_scope = enter_function_scope;
+   add_lvar_scope = add_lvar_scope;
+   open_scope = open_scope;
+   close_scope = close_scope;
+   start_live_range = start_live_range;
+   end_live_range = end_live_range;
+   stack_variable = stack_variable;
+   add_label = add_label;
+   atom_parameter = atom_parameter;
+   compute_diab_file_enum = compute_diab_file_enum;
+   compute_gnu_file_enum = compute_gnu_file_enum;
+   exists_section = exists_section;
+   remove_unused = remove_unused;
+   remove_unused_function = remove_unused_function;
+   variable_printed = variable_printed;
+   add_diab_info = (fun _ _ _ _ -> ());
+ }
diff --git a/debug/DebugInformation.mli b/debug/DebugInformation.mli
index a5d1f806..8905d8bf 100644
--- a/debug/DebugInformation.mli
+++ b/debug/DebugInformation.mli
@@ -11,7 +11,6 @@
 (* *********************************************************************)
 
 open BinNums
-open C
 open Camlcoq
 open DebugTypes
 open Sections
@@ -48,58 +47,10 @@ val file_name: string ref
 
 val fold_definitions: (int -> definition_type -> 'a -> 'a) -> 'a -> 'a
 
-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 diab_add_fun_addr: atom -> section_name -> (int * int) -> unit
 
 val gnu_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
-
-val enter_scope: int -> int -> int -> unit
-
-val enter_function_scope: int -> int -> unit
-
-val add_lvar_scope: int -> ident -> int -> unit
-
-val open_scope: atom -> int -> positive -> unit
-
-val close_scope: atom -> int -> positive -> unit
-
-val start_live_range: (atom * atom) -> positive -> (int * int AST.builtin_arg) -> unit
-
-val end_live_range: (atom * atom) -> positive -> unit
-
-val stack_variable: (atom * atom) -> int * int AST.builtin_arg -> unit
-
-val add_label: atom -> positive -> int -> unit
-
-val atom_parameter: ident -> ident -> atom -> 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: section_name -> bool
-
-val remove_unused: ident -> unit
-
-val remove_unused_function: ident -> unit
-
-val variable_printed: string -> unit
-
 val add_diab_info: section_name ->  int -> int  -> int -> unit
 
-val init: string -> unit
+val default_debug: Debug.implem
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml
index 94a8cf02..f35d7128 100644
--- a/debug/DebugInit.ml
+++ b/debug/DebugInit.ml
@@ -15,47 +15,16 @@ open Commandline
 open Debug
 open Driveraux
 
-let default_debug =
-  {
-   init = DebugInformation.init;
-   atom_global = DebugInformation.atom_global;
-   set_composite_size = DebugInformation.set_composite_size;
-   set_member_offset = DebugInformation.set_member_offset;
-   set_bitfield_offset = DebugInformation.set_bitfield_offset;
-   insert_global_declaration = DebugInformation.insert_global_declaration;
-   add_fun_addr = (fun _ _ _ -> ());
-   generate_debug_info = (fun _ _  -> None);
-   all_files_iter = DebugInformation.all_files_iter;
-   insert_local_declaration = DebugInformation.insert_local_declaration;
-   atom_local_variable = DebugInformation.atom_local_variable;
-   enter_scope = DebugInformation.enter_scope;
-   enter_function_scope = DebugInformation.enter_function_scope;
-   add_lvar_scope = DebugInformation.add_lvar_scope;
-   open_scope = DebugInformation.open_scope;
-   close_scope = DebugInformation.close_scope;
-   start_live_range = DebugInformation.start_live_range;
-   end_live_range = DebugInformation.end_live_range;
-   stack_variable = DebugInformation.stack_variable;
-   add_label = DebugInformation.add_label;
-   atom_parameter = DebugInformation.atom_parameter;
-   compute_diab_file_enum = DebugInformation.compute_diab_file_enum;
-   compute_gnu_file_enum = DebugInformation.compute_gnu_file_enum;
-   exists_section = DebugInformation.exists_section;
-   remove_unused = DebugInformation.remove_unused;
-   remove_unused_function = DebugInformation.remove_unused_function;
-   variable_printed = DebugInformation.variable_printed;
-   add_diab_info = (fun _ _ _ _ -> ());
- }
 
 let init_debug () =
   implem :=
   if Configuration.system = "diab" then
     let gen = (fun a b -> Some (Dwarfgen.gen_diab_debug_info a b)) in
-    {default_debug with generate_debug_info = gen;
+    {DebugInformation.default_debug with generate_debug_info = gen;
      add_diab_info = DebugInformation.add_diab_info;
      add_fun_addr = DebugInformation.diab_add_fun_addr;}
   else
-    {default_debug with generate_debug_info = (fun a b -> Some (Dwarfgen.gen_gnu_debug_info a b));
+    {DebugInformation.default_debug with generate_debug_info = (fun a b -> Some (Dwarfgen.gen_gnu_debug_info a b));
      add_fun_addr = DebugInformation.gnu_add_fun_addr}
 
 let init_none () =