aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DwarfUtil.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-17 18:19:37 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-17 18:19:37 +0200
commitc8a0b76c6b9c3eb004a7fccdd2ad15cc8615ef93 (patch)
treec9dacff414156d4d527ac40078cbdc51f160c8d0 /debug/DwarfUtil.ml
parent98cddc7ba45b34fbd71d9a80c27a8e5ec6b311b0 (diff)
downloadcompcert-kvx-c8a0b76c6b9c3eb004a7fccdd2ad15cc8615ef93.tar.gz
compcert-kvx-c8a0b76c6b9c3eb004a7fccdd2ad15cc8615ef93.zip
First version with computation of dwarf info from debug info.
Introduced a new dwarf generation from the information collected in the DebugInformation and removed the old CtODwarf translation.
Diffstat (limited to 'debug/DwarfUtil.ml')
-rw-r--r--debug/DwarfUtil.ml12
1 files changed, 1 insertions, 11 deletions
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
index e2c87a9d..d5e72adb 100644
--- a/debug/DwarfUtil.ml
+++ b/debug/DwarfUtil.ml
@@ -14,18 +14,8 @@
open DwarfTypes
-let id = ref 0
-
-let next_id () =
- let nid = !id in
- incr id; nid
-
-let reset_id () =
- id := 0
-
(* Generate a new entry from a given tag *)
-let new_entry tag =
- let id = next_id () in
+let new_entry id tag =
{
tag = tag;
children = [];