From c78b7a0562b93830f555f73e2fbe10469e1e14f0 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 23 Oct 2014 18:26:44 +0200 Subject: Added a file for utility functions on the Dwarf types. --- debug/DwarfUtil.ml | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 debug/DwarfUtil.ml (limited to 'debug/DwarfUtil.ml') diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml new file mode 100644 index 00000000..3841caa5 --- /dev/null +++ b/debug/DwarfUtil.ml @@ -0,0 +1,32 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Utility functions for the dwarf debuging type *) + +open DwarfTypes + +let id = ref 0 + +let next_id () = + let nid = !id in + incr id; nid + +let new_entry tag = + let id = next_id () in + { + tag = tag; + children = []; + id = id; + } + +let add_children entry child = + {entry with children = child::entry.children;} -- cgit