aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintAsmaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/PrintAsmaux.ml')
-rw-r--r--backend/PrintAsmaux.ml10
1 files changed, 4 insertions, 6 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index a67c85d2..3f0b3ea3 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -48,9 +48,13 @@ module type TARGET =
val get_start_addr: unit -> int
val get_end_addr: unit -> int
val get_stmt_list_addr: unit -> int
+ val get_debug_start_addr: unit -> int
val new_label: unit -> int
val label: out_channel -> int -> unit
val print_file_loc: out_channel -> file_loc -> unit
+ val get_location: P.t -> location_value option
+ val get_segment_location: P.t -> location_value option
+ val add_var_location: P.t -> unit
module DwarfAbbrevs: DWARF_ABBREVS
end
@@ -140,12 +144,6 @@ let coqint oc n =
fprintf oc "%ld" (camlint_of_coqint n)
(* Printing annotations in asm syntax *)
-(** All files used in the debug entries *)
-module StringSet = Set.Make(String)
-let all_files : StringSet.t ref = ref StringSet.empty
-let add_file file =
- all_files := StringSet.add file !all_files
-
let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
= Hashtbl.create 7