From d9c0c49cf32be6aa17918654c05bee45f29fb737 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 18 Mar 2016 13:17:09 +0100
Subject: Added an interface file for DebugInformation.

The interface hides the implementation details, like the huge
number of Hashtbls from the rest of the implementatio.
Bug 18394
---
 debug/DebugTypes.mli | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'debug/DebugTypes.mli')

diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli
index 53a39665..25c7390f 100644
--- a/debug/DebugTypes.mli
+++ b/debug/DebugTypes.mli
@@ -10,6 +10,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open AST
+open BinNums
 open C
 open Camlcoq
 
@@ -158,3 +160,21 @@ type scope_information =
 type local_information =
   | LocalVariable of local_variable_information
   | Scope of scope_information
+
+
+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 *)
-- 
cgit