aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/TargetPrinter.ml1
-rw-r--r--backend/PrintAsm.ml4
-rw-r--r--backend/PrintAsmaux.ml71
-rw-r--r--debug/CtoDwarf.ml2
-rw-r--r--debug/Debug.ml86
-rw-r--r--debug/DwarfPrinter.mli1
-rw-r--r--ia32/TargetPrinter.ml1
-rw-r--r--powerpc/TargetPrinter.ml5
8 files changed, 95 insertions, 76 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 028ff6ed..d0e07958 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -20,6 +20,7 @@ open AST
open Memdata
open Asm
open PrintAsmaux
+open Debug
(* Type for the ABI versions *)
type float_abi_type =
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]*"
diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
index 063b0823..e37c6043 100644
--- a/debug/CtoDwarf.ml
+++ b/debug/CtoDwarf.ml
@@ -477,7 +477,7 @@ let union_to_dwarf (n,at,m) env gloc =
(* Translate global declarations to there dwarf representation *)
let globdecl_to_dwarf env (typs,decls) decl =
- PrintAsmaux.add_file (fst decl.gloc);
+ Debug.add_file (fst decl.gloc);
match decl.gdesc with
| Gtypedef (n,t) -> let ret = typedef_to_dwarf (Some decl.gloc) (n.name,t) in
typs@ret,decls
diff --git a/debug/Debug.ml b/debug/Debug.ml
new file mode 100644
index 00000000..dfe7fd94
--- /dev/null
+++ b/debug/Debug.ml
@@ -0,0 +1,86 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+open Printf
+
+(* 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
diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli
index 9e0e6693..ccdecffb 100644
--- a/debug/DwarfPrinter.mli
+++ b/debug/DwarfPrinter.mli
@@ -1,3 +1,4 @@
+
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index d1e213e2..9227929b 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -20,6 +20,7 @@ open AST
open Memdata
open Asm
open PrintAsmaux
+open Debug
module StringSet = Set.Make(String)
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 409f2cc0..5159850d 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -21,6 +21,7 @@ open AST
open Memdata
open Asm
open PrintAsmaux
+open Debug
(* Recognition of target ABI and asm syntax *)
@@ -139,7 +140,7 @@ module Linux_System : SYSTEM =
let print_file_line oc file line =
- print_file_line oc comment file line
+ Debug.print_file_line oc comment file line
(* Emit .cfi directives *)
let cfi_startproc = cfi_startproc
@@ -217,7 +218,7 @@ module Diab_System : SYSTEM =
let print_file_line oc file line =
- print_file_line_d2 oc comment file line
+ Debug.print_file_line_d2 oc comment file line
(* Emit .cfi directives *)
let cfi_startproc oc = ()
generated by cgit (git 2.34.1) at 2024-06-02 21:02:21 +0000