aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintAsmaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/PrintAsmaux.ml')
-rw-r--r--backend/PrintAsmaux.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index aa0f4214..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
@@ -46,6 +47,10 @@ module type TARGET =
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 *)