aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DwarfPrinter.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-04-14 16:18:46 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-04-14 16:18:46 +0200
commite42febd5a88c2bf04227f1cd4ead947c51989ec1 (patch)
tree0661131709c95dc77a5c0583f66caf219a84e8cf /debug/DwarfPrinter.mli
parent03ad26aa9d2762655b508f7142d0aed9916da83b (diff)
parentb597ce896a8a9cd7c3ed028a34e0612229d1a36a (diff)
downloadcompcert-kvx-e42febd5a88c2bf04227f1cd4ead947c51989ec1.tar.gz
compcert-kvx-e42febd5a88c2bf04227f1cd4ead947c51989ec1.zip
Merge branch 'dwarf' of /local/schommer/trunk/build/compcert.ppc/compcert into dwarf
Diffstat (limited to 'debug/DwarfPrinter.mli')
-rw-r--r--debug/DwarfPrinter.mli18
1 files changed, 18 insertions, 0 deletions
diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli
new file mode 100644
index 00000000..9e0e6693
--- /dev/null
+++ b/debug/DwarfPrinter.mli
@@ -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. *)
+(* *)
+(* *********************************************************************)
+
+open DwarfTypes
+
+module DwarfPrinter: functor (Target: DWARF_TARGET) -> functor (DwarfAbbrevs: DWARF_ABBREVS) ->
+ sig
+ val print_debug: out_channel -> dw_entry -> unit
+ end