Moved the types defined by the Debug Interface into a separate file.

3 files changed, 163 insertions, 146 deletions

diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 1fe1a805..40cc4060 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -15,6 +15,7 @@ open BinNums
 open C
 open Camlcoq
 open Cutil
+open DebugTypes
 
 (* This implements an interface for the collection of debugging 
    information. *)
@@ -42,96 +43,6 @@ let all_files : StringSet.t ref = ref StringSet.empty
 let add_file file =
   all_files := StringSet.add file !all_files
 
-(* Types for the information of type info *)
-type composite_field =
-    {
-     cfd_name:        string;
-     cfd_typ:         int;
-     cfd_bit_size:    int option;
-     cfd_bit_offset:  int option;
-     cfd_byte_offset: int option;
-     cfd_byte_size:   int option;
-     cfd_bitfield:    string option;
-   }
-
-type composite_type =
-    {
-     ct_name:        string;
-     ct_sou:         struct_or_union;
-     ct_file_loc:    location option;
-     ct_members:     composite_field list;
-     ct_sizeof:      int option;
-     ct_declaration: bool;
-   }
-
-type ptr_type = {
-    pts: int
-  }
-
-type const_type = {
-    cst_type: int
-  }
-
-type volatile_type = {
-    vol_type: int
-  }
-
-
-type array_type = {
-    arr_type: int;
-    arr_size: int64 option list;
-  }
-
-type typedef = {
-    typedef_file_loc: location option;
-    typedef_name:     string;
-    typ:              int option;
-  }
-
-type enumerator = {
-    enumerator_name:     string;
-    enumerator_const:    int64;
-  }
-
-type enum_type = {
-    enum_name:        string;
-    enum_byte_size:   int option;
-    enum_file_loc:    location option;
-    enum_enumerators: enumerator list; 
-  }
-
-type int_type = {
-    int_kind: ikind;
-  }
-
-type float_type = {
-    float_kind: fkind;
-  }
-
-type parameter_type = {
-    param_type: int;
-    param_name: string;
-  }
-
-type function_type = {
-    fun_return_type: int option;
-    fun_prototyped:  bool;
-    fun_params:      parameter_type list;
-  }
-
-type debug_types =
-  | IntegerType of int_type
-  | FloatType of float_type
-  | PointerType of ptr_type
-  | ArrayType of array_type
-  | CompositeType of composite_type
-  | EnumType of enum_type
-  | FunctionType of function_type
-  | Typedef of typedef
-  | ConstType of const_type
-  | VolatileType of volatile_type
-  | Void
-
 (* All types encountered *)
 let types: (int,debug_types) Hashtbl.t = Hashtbl.create 7
 
@@ -343,43 +254,6 @@ let replace_typedef id f =
     if typ <> typ' then Hashtbl.replace types id (Typedef typ')
   | _ -> assert false (* This should never happen *)
 
-(* Types for global definitions *)
-
-(* Information for a global variable *)
-type global_variable_information = {
-    gvar_name:        string;
-    gvar_atom:        atom option;
-    gvar_file_loc:    location;
-    gvar_declaration: bool;
-    gvar_external:    bool;
-    gvar_type:        int;
-  }
-
-type parameter_information = 
- {
-  parameter_name:     string;
-  parameter_ident:    int;
-  parameter_atom:     atom option;
-  parameter_type:     int;
-}
-
-type function_information = {
-    fun_name:        string;
-    fun_atom:        atom option;
-    fun_file_loc:    location;
-    fun_external:    bool;
-    fun_return_type: int option; (* Again the special case of void functions *)
-    fun_vararg:      bool;
-    fun_parameter:   parameter_information list;
-    fun_low_pc:      int option;
-    fun_high_pc:     int option;
-    fun_scope:       int option;
-  }
-
-type definition_type =
-  | GlobalVariable of global_variable_information
-  | Function of function_information
-
 
 (* All global definitions encountered *)
 let definitions: (int,definition_type) Hashtbl.t = Hashtbl.create 7
@@ -422,25 +296,6 @@ let replace_fun id f =
   let f = Function f in
   Hashtbl.replace definitions id f
 
-
-(* Information for local variables *)
-type local_variable_information = {
-    lvar_name:    string;
-    lvar_atom:    atom option;
-    lvar_file_loc:location;
-    lvar_type:    int;
-    lvar_static:  bool;  (* Static variable are mapped to symbols *)
-  }
-
-type scope_information = 
-  {
-   scope_variables: int list; (* Variable and Scope ids *)
- }
-
-type local_information =
-  | LocalVariable of local_variable_information
-  | Scope of scope_information
-
 (* All local variables *)
 let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7
 
diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli
new file mode 100644
index 00000000..6a4f619c
--- /dev/null
+++ b/debug/DebugTypes.mli
@@ -0,0 +1,160 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open C
+open Camlcoq
+
+(* Types for the information of type info *)
+type composite_field =
+    {
+     cfd_name:        string;
+     cfd_typ:         int;
+     cfd_bit_size:    int option;
+     cfd_bit_offset:  int option;
+     cfd_byte_offset: int option;
+     cfd_byte_size:   int option;
+     cfd_bitfield:    string option;
+   }
+
+type composite_type =
+    {
+     ct_name:        string;
+     ct_sou:         struct_or_union;
+     ct_file_loc:    location option;
+     ct_members:     composite_field list;
+     ct_sizeof:      int option;
+     ct_declaration: bool;
+   }
+
+type ptr_type = {
+    pts: int
+  }
+
+type const_type = {
+    cst_type: int
+  }
+
+type volatile_type = {
+    vol_type: int
+  }
+
+
+type array_type = {
+    arr_type: int;
+    arr_size: int64 option list;
+  }
+
+type typedef = {
+    typedef_file_loc: location option;
+    typedef_name:     string;
+    typ:              int option;
+  }
+
+type enumerator = {
+    enumerator_name:     string;
+    enumerator_const:    int64;
+  }
+
+type enum_type = {
+    enum_name:        string;
+    enum_byte_size:   int option;
+    enum_file_loc:    location option;
+    enum_enumerators: enumerator list; 
+  }
+
+type int_type = {
+    int_kind: ikind;
+  }
+
+type float_type = {
+    float_kind: fkind;
+  }
+
+type parameter_type = {
+    param_type: int;
+    param_name: string;
+  }
+
+type function_type = {
+    fun_return_type: int option;
+    fun_prototyped:  bool;
+    fun_params:      parameter_type list;
+  }
+
+type debug_types =
+  | IntegerType of int_type
+  | FloatType of float_type
+  | PointerType of ptr_type
+  | ArrayType of array_type
+  | CompositeType of composite_type
+  | EnumType of enum_type
+  | FunctionType of function_type
+  | Typedef of typedef
+  | ConstType of const_type
+  | VolatileType of volatile_type
+  | Void
+
+(* Types for global definitions *)
+
+(* Information for a global variable *)
+type global_variable_information = {
+    gvar_name:        string;
+    gvar_atom:        atom option;
+    gvar_file_loc:    location;
+    gvar_declaration: bool;
+    gvar_external:    bool;
+    gvar_type:        int;
+  }
+
+type parameter_information = 
+ {
+  parameter_name:     string;
+  parameter_ident:    int;
+  parameter_atom:     atom option;
+  parameter_type:     int;
+}
+
+type function_information = {
+    fun_name:        string;
+    fun_atom:        atom option;
+    fun_file_loc:    location;
+    fun_external:    bool;
+    fun_return_type: int option; (* Again the special case of void functions *)
+    fun_vararg:      bool;
+    fun_parameter:   parameter_information list;
+    fun_low_pc:      int option;
+    fun_high_pc:     int option;
+    fun_scope:       int option;
+  }
+
+type definition_type =
+  | GlobalVariable of global_variable_information
+  | Function of function_information
+
+
+(* Information for local variables *)
+type local_variable_information = {
+    lvar_name:    string;
+    lvar_atom:    atom option;
+    lvar_file_loc:location;
+    lvar_type:    int;
+    lvar_static:  bool;  (* Static variable are mapped to symbols *)
+  }
+
+type scope_information = 
+  {
+   scope_variables: int list; (* Variable and Scope ids *)
+ }
+
+type local_information =
+  | LocalVariable of local_variable_information
+  | Scope of scope_information
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index 6c79ce0c..1ef00c31 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -15,8 +15,10 @@ open C
 open Camlcoq
 open Cutil
 open DebugInformation
+open DebugTypes
 open DwarfTypes
 open DwarfUtil
+
 (* Generate the dwarf DIE's from the information collected in DebugInformation *)
 
 (* Helper function to get values that must be set. *)