aboutsummaryrefslogtreecommitdiffstats
path: root/debug/DwarfPrinter.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2015-04-15 12:15:12 +0200
committerBernhard Schommer <bschommer@users.noreply.github.com>2015-04-15 12:15:12 +0200
commit1150b687acf225e0f6063de45379c3d5fbc54524 (patch)
tree0661131709c95dc77a5c0583f66caf219a84e8cf /debug/DwarfPrinter.mli
parent03ad26aa9d2762655b508f7142d0aed9916da83b (diff)
parente42febd5a88c2bf04227f1cd4ead947c51989ec1 (diff)
downloadcompcert-1150b687acf225e0f6063de45379c3d5fbc54524.tar.gz
compcert-1150b687acf225e0f6063de45379c3d5fbc54524.zip
Merge pull request #37 from AbsInt/dwarf
Added the Dwarf v2 debugging information for global variables and functions for the Diab Backend.
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