aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-03-16 12:23:29 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-03-16 12:23:29 +0100
commitb3c67667b7121b7f2e50700ec6da4bd780dee426 (patch)
treefbd6cfe3b6cfda555ca9389e58a2b226df480013 /backend
parenta84576b219c797467e480508fc99ba78260062df (diff)
downloadcompcert-kvx-b3c67667b7121b7f2e50700ec6da4bd780dee426.tar.gz
compcert-kvx-b3c67667b7121b7f2e50700ec6da4bd780dee426.zip
Started implementing the printing functions for the debug info. Added a global target dependend option to activate the printing only for targets wher it works.
Diffstat (limited to 'backend')
-rw-r--r--backend/PrintAsm.ml7
-rw-r--r--backend/PrintAsmaux.ml5
2 files changed, 11 insertions, 1 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index a48bd910..a394cf8e 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -99,4 +99,9 @@ let print_program oc p =
Target.print_prologue oc;
List.iter (Printer.print_globdef oc) p.prog_defs;
Target.print_epilogue oc;
- PrintAnnot.close_filenames ()
+ PrintAnnot.close_filenames ();
+ if !Clflags.option_g && Configuration.advanced_debug then
+ begin
+ let module DebugPrinter = DwarfPrinter(Target) in
+ ()
+ end
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index aa0f4214..8bc961ef 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -14,6 +14,7 @@
open AST
open Asm
open Camlcoq
+open DwarfTypes
open Datatypes
open Printf
open Sections
@@ -46,6 +47,10 @@ module type TARGET =
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 *)