aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintAsmaux.ml
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 /backend/PrintAsmaux.ml
parent03ad26aa9d2762655b508f7142d0aed9916da83b (diff)
parentb597ce896a8a9cd7c3ed028a34e0612229d1a36a (diff)
downloadcompcert-e42febd5a88c2bf04227f1cd4ead947c51989ec1.tar.gz
compcert-e42febd5a88c2bf04227f1cd4ead947c51989ec1.zip
Merge branch 'dwarf' of /local/schommer/trunk/build/compcert.ppc/compcert into dwarf
Diffstat (limited to 'backend/PrintAsmaux.ml')
-rw-r--r--backend/PrintAsmaux.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 64db2cb0..8bc961ef 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -14,6 +14,7 @@
open AST
open Asm
open Camlcoq
+open DwarfTypes
open Datatypes
open Printf
open Sections
@@ -43,6 +44,13 @@ module type TARGET =
val comment: string
val symbol: out_channel -> P.t -> unit
val default_falignment: int
+ val get_start_addr: unit -> int
+ val get_end_addr: unit -> int
+ val get_stmt_list_addr: unit -> int
+ val new_label: unit -> int
+ val label: out_channel -> int -> unit
+ val print_file_loc: out_channel -> file_loc -> unit
+ module DwarfAbbrevs: DWARF_ABBREVS
end
(* On-the-fly label renaming *)