From 861292a6c5e58b4f78bef207c717b801b3fc1fed Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Sun, 6 Sep 2015 20:32:55 +0200
Subject: Startet implementation of new Debug interface.

Added a new file debug/Debug.ml which will be the interface between for
generating and printing the debuging information. Currently it contains
only the code for the line directived.
---
 backend/PrintAsm.ml    |  4 +--
 backend/PrintAsmaux.ml | 71 --------------------------------------------------
 2 files changed, 2 insertions(+), 73 deletions(-)

(limited to 'backend')

diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 29409b32..b88a3d50 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -134,12 +134,12 @@ module Printer(Target:TARGET) =
 let print_program oc p db =
   let module Target = (val (sel_target ()):TARGET) in
   let module Printer = Printer(Target) in
-  reset_filenames ();
+  Debug.reset_filenames ();
   print_version_and_options oc Target.comment;
   Target.print_prologue oc;
   List.iter (Printer.print_globdef oc) p.prog_defs;
   Target.print_epilogue oc;
-  close_filenames ();
+  Debug.close_filenames ();
   if !Clflags.option_g && Configuration.advanced_debug then
     begin
       match db with
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 324e7e66..441f8251 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -142,77 +142,6 @@ 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]*"
-- 
cgit