diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-10-23 18:26:44 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-10-23 18:26:44 +0200 |
commit | c78b7a0562b93830f555f73e2fbe10469e1e14f0 (patch) | |
tree | fa846c96dc9bb519af0c1205c6dd4924680244bf /debug/DwarfUtil.ml | |
parent | b483cbe0304ff7571668d0c703b8271bbbe8323c (diff) | |
download | compcert-c78b7a0562b93830f555f73e2fbe10469e1e14f0.tar.gz compcert-c78b7a0562b93830f555f73e2fbe10469e1e14f0.zip |
Added a file for utility functions on the Dwarf types.
Diffstat (limited to 'debug/DwarfUtil.ml')
-rw-r--r-- | debug/DwarfUtil.ml | 32 |
1 files changed, 32 insertions, 0 deletions
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;} |