Revert "Startet implementation of new Debug interface."

This reverts commit 861292a6c5e58b4f78bef207c717b801b3fc1fed.

1 files changed, 71 insertions, 0 deletions

diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 441f8251..324e7e66 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -142,6 +142,77 @@ let cfi_rel_offset =
 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
+
+let last_file = ref ""
+
+let reset_filenames () =
+  Hashtbl.clear filename_info; last_file := ""
+
+let close_filenames () =
+  Hashtbl.iter
+    (fun file (num, fb) ->
+       match fb with Some b -> Printlines.close b | None -> ())
+    filename_info;
+  reset_filenames()
+
+let enter_filename f =
+  let num = Hashtbl.length filename_info + 1 in
+  let filebuf =
+    if !Clflags.option_S || !Clflags.option_dasm then begin
+      try Some (Printlines.openfile f)
+      with Sys_error _ -> None
+    end else None in
+  Hashtbl.add filename_info f (num, filebuf);
+  (num, filebuf)
+
+(* Add file and line debug location, using GNU assembler-style DWARF2
+   directives *)
+
+let print_file_line oc pref file line =
+  if !Clflags.option_g && file <> "" then begin
+    let (filenum, filebuf) =
+      try
+        Hashtbl.find filename_info file
+      with Not_found ->
+        let (filenum, filebuf as res) = enter_filename file in
+        fprintf oc "	.file	%d %S\n" filenum file;
+        res in
+    fprintf oc "	.loc	%d %d\n" filenum line;
+    match filebuf with
+    | None -> ()
+    | Some fb -> Printlines.copy oc pref fb line line
+  end
+
+(* Add file and line debug location, using DWARF2 directives in the style
+   of Diab C 5 *)
+
+let print_file_line_d2 oc pref file line =
+  if !Clflags.option_g && file <> "" then begin
+    let (_, filebuf) =
+      try
+        Hashtbl.find filename_info file
+      with Not_found ->
+        enter_filename file in
+    if file <> !last_file then begin
+      fprintf oc "	.d2file	%S\n" file;
+      last_file := file
+    end;
+    fprintf oc "	.d2line	%d\n" line;
+    match filebuf with
+    | None -> ()
+    | Some fb -> Printlines.copy oc pref fb line line
+  end
+
 (** Programmer-supplied annotations (__builtin_annot). *)
 
 let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"