From c8a0b76c6b9c3eb004a7fccdd2ad15cc8615ef93 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 17 Sep 2015 18:19:37 +0200
Subject: First version with computation of dwarf info from debug info.

Introduced a new dwarf generation from the information collected in
the DebugInformation and removed the old CtODwarf translation.
---
 backend/PrintAsm.ml    | 9 ++++-----
 backend/PrintAsmaux.ml | 6 ------
 2 files changed, 4 insertions(+), 11 deletions(-)

(limited to 'backend')

diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index ea3d985a..9ffe3aa5 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -27,9 +27,9 @@ module Printer(Target:TARGET) =
     let addr_mapping: (string, (int * int)) Hashtbl.t = Hashtbl.create 7
 
     let get_fun_addr name =
-      let s = new_label ()
-      and e = new_label () in
-      Debug.add_fun_addr name (s,e);
+      let s = Target.new_label ()
+      and e = Target.new_label () in
+      Debug.add_fun_addr name (e,s);
       s,e
 
     let print_debug_label oc l =
@@ -118,7 +118,6 @@ module Printer(Target:TARGET) =
         let get_end_addr = Target.get_end_addr
         let get_stmt_list_addr = Target.get_stmt_list_addr
         let name_of_section = Target.name_of_section
-        let get_fun_addr s = try Some (Hashtbl.find addr_mapping s) with Not_found -> None
         let get_location a =  None
         let get_frame_base a = None
         let symbol = Target.symbol
@@ -140,7 +139,7 @@ let print_program oc p db =
   close_filenames ();
   if !Clflags.option_g && Configuration.advanced_debug then
     begin
-      match db with
+      match Debug.generate_debug_info () with
       | None -> ()
       | Some db ->
           Printer.DebugPrinter.print_debug oc db
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 324e7e66..2daa2d56 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -143,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
-- 
cgit