From 2d96b7927719c3b61fe564e8ab273a1b154912a5 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 1 Oct 2015 19:16:59 +0200
Subject: Moved the types defined by the Debug Interface into a separate file.

---
 debug/DebugTypes.mli | 160 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 160 insertions(+)
 create mode 100644 debug/DebugTypes.mli

(limited to 'debug/DebugTypes.mli')

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
-- 
cgit