1 files changed, 30 insertions, 18 deletions

diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index e8f1703a..828759a7 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -10,7 +10,6 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-open AST
 open BinNums
 open C
 open Camlcoq
@@ -47,6 +46,10 @@ let add_file file =
 (* All types encountered *)
 let types: (int,debug_types) Hashtbl.t = Hashtbl.create 7
 
+let get_type = Hashtbl.find types
+
+let fold_types f a = Hashtbl.fold f types a
+
 (* Lookup table for types *)
 let lookup_types: (string, int) Hashtbl.t = Hashtbl.create 7
 
@@ -213,6 +216,8 @@ let replace_typedef id f =
 (* All global definitions encountered *)
 let definitions: (int,definition_type) Hashtbl.t = Hashtbl.create 7
 
+let fold_definitions f a  = Hashtbl.fold f definitions a
+
 (* Mapping from stamp to debug id *)
 let stamp_to_definition: (int,int) Hashtbl.t = Hashtbl.create 7
 
@@ -255,6 +260,8 @@ let replace_fun id f =
 (* All local variables *)
 let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7
 
+let get_local_variable id = Hashtbl.find local_variables id
+
 (* Mapping from stamp to the debug id of the local variable *)
 let stamp_to_local: (int,int) Hashtbl.t = Hashtbl.create 7
 
@@ -516,29 +523,18 @@ let enter_scope f_id p_id id =
   with Not_found  -> ()
 
 
-type scope_range =
-    {
-     start_addr: positive option;
-     end_addr: positive option;
-   }
-
-type var_range =
-    {
-     range_start: positive option;
-     range_end:   positive option;
-     var_loc:     int * int builtin_arg;
-   }
-
-type var_location =
-  | RangeLoc of var_range list
-  | FunctionLoc of  int * int builtin_arg (* Stack allocated variables *)
-
 let var_locations: (atom * atom,var_location) Hashtbl.t = Hashtbl.create 7
 
+let variable_location var f = Hashtbl.find var_locations (var,f)
+
 let scope_ranges: (int,scope_range list) Hashtbl.t = Hashtbl.create 7
 
+let get_scope_ranges = Hashtbl.find scope_ranges
+
 let label_translation: (atom * positive, int) Hashtbl.t = Hashtbl.create 7
 
+let translate_label f l = Hashtbl.find label_translation (f,l)
+
 let add_label atom p i =
   Hashtbl.add label_translation (atom,p) i
 
@@ -589,8 +585,18 @@ let stack_variable (f,v) (sp,loc) =
 let compilation_section_start: (string,int) Hashtbl.t = Hashtbl.create 7
 let compilation_section_end: (string,int) Hashtbl.t = Hashtbl.create 7
 
+let section_start n = Hashtbl.find compilation_section_start n
+
+let fold_section_start f a =  Hashtbl.fold f compilation_section_start a
+
+let section_end n = Hashtbl.find compilation_section_end n
+
 let diab_additional: (string,int * int * section_name) Hashtbl.t = Hashtbl.create 7
 
+let diab_additional_section s =
+  let line_start,debug_start,_ = Hashtbl.find diab_additional s in
+  line_start,debug_start
+
 let section_to_string = function
   | Section_user (n,_,_) -> n
   | _ -> ".text"
@@ -622,6 +628,8 @@ let exists_section sec =
 
 let filenum: (string * string,int) Hashtbl.t = Hashtbl.create 7
 
+let diab_file_loc f l = Hashtbl.find filenum (f,l)
+
 let compute_diab_file_enum end_label entry_label line_end =
   Hashtbl.iter (fun sec (_,_,secname) ->
     Hashtbl.add compilation_section_end sec (end_label secname);
@@ -633,8 +641,12 @@ let compute_diab_file_enum end_label entry_label line_end =
 let compute_gnu_file_enum f =
   StringSet.iter f !all_files
 
+let all_files_iter f = StringSet.iter f !all_files
+
 let printed_vars: StringSet.t ref = ref StringSet.empty
 
+let is_variable_printed id = StringSet.mem id !printed_vars
+
 let variable_printed id =
   printed_vars := StringSet.add id !printed_vars