aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-03-16 18:09:15 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-03-16 18:09:15 +0100
commit89e7840807d9b39636ed84c43ec21485ea776cf9 (patch)
treeb7019fd505fe5daa369a798c12ff91f9362e860b /debug
parent9699d81b304414534008258c05d391bdc1c9e217 (diff)
downloadcompcert-kvx-89e7840807d9b39636ed84c43ec21485ea776cf9.tar.gz
compcert-kvx-89e7840807d9b39636ed84c43ec21485ea776cf9.zip
Added file for the translation of the C Ast to Dwarf debugging information.
Diffstat (limited to 'debug')
-rw-r--r--debug/CtoDwarf.ml18
-rw-r--r--debug/DwarfUtil.ml7
2 files changed, 18 insertions, 7 deletions
diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
new file mode 100644
index 00000000..0ee0842a
--- /dev/null
+++ b/debug/CtoDwarf.ml
@@ -0,0 +1,18 @@
+(* *********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(* *********************************************************************)
+
+(* Functions to translate a C Ast into Dwarf 2 debugging information *)
+
+
+(* Hashtable to from type name to entry id *)
+let type_table: (string, int) Hashtbl.t = Hashtbl.create 7
+
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
index b3cef748..764194a6 100644
--- a/debug/DwarfUtil.ml
+++ b/debug/DwarfUtil.ml
@@ -23,13 +23,6 @@ let next_id () =
let reset_id () =
id := 0
-(* Hashtable to from type name to entry id *)
-let type_table: (string, int) Hashtbl.t = Hashtbl.create 7
-
-(* Clear the type map *)
-let reset_type_table () =
- Hashtbl.clear type_table
-
(* Generate a new entry from a given tag *)
let new_entry tag =
let id = next_id () in