1 files changed, 9 insertions, 78 deletions

diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 67e53aea..78399c04 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -14,7 +14,6 @@
 open AST
 open Asm
 open Camlcoq
-open DwarfTypes
 open Datatypes
 open Memdata
 open Printf
@@ -45,13 +44,8 @@ module type TARGET =
       val comment: string
       val symbol: out_channel -> P.t -> unit
       val default_falignment: int
-      val get_start_addr: unit -> int
-      val get_end_addr: unit -> int
-      val get_stmt_list_addr: unit -> int
       val new_label: unit -> int
       val label: out_channel -> int -> unit
-      val print_file_loc: out_channel -> file_loc -> unit
-      module DwarfAbbrevs:  DWARF_ABBREVS
     end
 
 (* On-the-fly label renaming *)
@@ -139,77 +133,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]*"
@@ -283,6 +206,9 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args =
   | 5 ->  (* local variable preallocated in stack *)
       fprintf oc "%s debug: %s resides at%a\n"
                  comment txt print_debug_args args
+  | 6 ->  (* scope annotations *)
+      fprintf oc "%s debug: current scopes%a\n"
+                 comment print_debug_args args;
   | _ ->
       ()
 					    
@@ -330,7 +256,12 @@ let print_inline_asm print_preg oc txt sg args res =
 (** Print CompCert version and command-line as asm comment *)
 
 let print_version_and_options oc comment =
-  fprintf oc "%s File generated by CompCert %s\n" comment Version.version;
+  let version_string =  
+    if Version.buildnr <> "" && Version.tag <> "" then
+      sprintf "%s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
+    else
+      Version.version in
+  fprintf oc "%s File generated by CompCert %s\n" comment version_string;
   fprintf oc "%s Command line:" comment;
   for i = 1 to Array.length Sys.argv - 1 do
     fprintf oc " %s" Sys.argv.(i)