diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-18 13:17:09 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-18 13:17:09 +0100 |
| commit | d9c0c49cf32be6aa17918654c05bee45f29fb737 (patch) | |
| tree | d9f0f034c48553840126414ee9daca4d018ece16 /debug/DebugTypes.mli | |
| parent | 1e08d4adb241e076a96f9525fdb8359cf8845527 (diff) | |
| download | compcert-kvx-d9c0c49cf32be6aa17918654c05bee45f29fb737.tar.gz compcert-kvx-d9c0c49cf32be6aa17918654c05bee45f29fb737.zip | |
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
Diffstat (limited to 'debug/DebugTypes.mli')
| -rw-r--r-- | debug/DebugTypes.mli | 20 |
1 files changed, 20 insertions, 0 deletions
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 *) |