aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintAsmaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/PrintAsmaux.ml')
-rw-r--r--backend/PrintAsmaux.ml9
1 files changed, 3 insertions, 6 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 13daa644..ed0fe524 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -51,6 +51,9 @@ module type TARGET =
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 +143,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