Merge branch 'dwarf' of /local/schommer/trunk/build/compcert.ppc/compcert into dwarf

3 files changed, 21 insertions, 12 deletions

diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 237085de..2cea2b80 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -93,6 +93,12 @@ let asm_supports_cfi =
   | "false" -> false
   | v -> bad_config "asm_supports_cfi" [v]
 
+let advanced_debug =
+  match get_config_string "advanced_debug" with
+  | "true" -> true
+  | "false" -> false
+  | v -> bad_config "advanced_debug" [v]
+
 let version = get_config_string "version"
 
 type struct_passing_style =
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index 875bd692..20c45518 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -31,6 +31,8 @@ val stdlib_path: string
   (** Path to CompCert's library *)
 val has_runtime_lib: bool
   (** True if CompCert's library is available. *)
+val advanced_debug: bool
+  (** True if advanced debug is implement for the Target *)
 
 val version: string
   (** CompCert version string *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index ad7cf61e..d225ec4f 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -117,17 +117,17 @@ let parse_c_file sourcename ifile =
   ^ (if !option_fpacked_structs then "p" else "")
   in
   (* Parsing and production of a simplified C AST *)
-  let ast =
+  let ast,debug =
     match Parse.preprocessed_file simplifs sourcename ifile with
-    | None -> exit 2
-    | Some p -> p in
+    | None,_ -> exit 2
+    | Some p,d -> p,d in
   (* Save C AST if requested *)
   if !option_dparse then begin
     let ofile = output_filename sourcename ".c" ".parsed.c" in
     let oc = open_out ofile in
     Cprint.program (Format.formatter_of_out_channel oc) ast;
     close_out oc
-  end;
+  end; 
   (* Conversion to Csyntax *)
   let csyntax =
     match Timing.time "CompCert C generation" C2C.convertProgram ast with
@@ -141,7 +141,7 @@ let parse_c_file sourcename ifile =
     PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
     close_out oc
   end;
-  csyntax
+  csyntax,debug
 
 (* Dump Asm code in binary format for the validator *)
 
@@ -157,7 +157,7 @@ let dump_asm asm destfile =
 
 (* From CompCert C AST to asm *)
 
-let compile_c_ast sourcename csyntax ofile =
+let compile_c_ast sourcename csyntax ofile debug =
   (* Prepare to dump Clight, RTL, etc, if requested *)
   let set_dest dst opt ext =
     dst := if !opt then Some (output_filename sourcename ".c" ext)
@@ -181,13 +181,14 @@ let compile_c_ast sourcename csyntax ofile =
     dump_asm asm (output_filename sourcename ".c" ".sdump");
   (* Print Asm in text form *)
   let oc = open_out ofile in
-  PrintAsm.print_program oc asm;
+  PrintAsm.print_program oc asm debug;
   close_out oc
 
 (* From C source to asm *)
 
 let compile_c_file sourcename ifile ofile =
-  compile_c_ast sourcename (parse_c_file sourcename ifile) ofile
+  let ast,debug = parse_c_file sourcename ifile in
+  compile_c_ast sourcename ast ofile debug
 
 (* From Cminor to asm *)
 
@@ -212,7 +213,7 @@ let compile_cminor_file ifile ofile =
         exit 2
     | Errors.OK p ->
         let oc = open_out ofile in
-        PrintAsm.print_program oc p;
+        PrintAsm.print_program oc p None;
         close_out oc
   with Parsing.Parse_error ->
          eprintf "File %s, character %d: Syntax error\n"
@@ -266,7 +267,7 @@ let process_c_file sourcename =
     preprocess sourcename preproname;
     if !option_interp then begin
       Machine.config := Machine.compcert_interpreter !Machine.config;
-      let csyntax = parse_c_file sourcename preproname in
+      let csyntax,_ = parse_c_file sourcename preproname in
       safe_remove preproname;
       Interp.execute csyntax;
       ""
@@ -293,7 +294,7 @@ let process_c_file sourcename =
 
 let process_i_file sourcename =
   if !option_interp then begin
-    let csyntax = parse_c_file sourcename sourcename in
+    let csyntax,_ = parse_c_file sourcename sourcename in
     Interp.execute csyntax;
     ""
   end else if !option_S then begin
@@ -514,7 +515,7 @@ let cmdline_actions =
   Exact "-fall", Self (fun _ -> set_all language_support_options);
   Exact "-fnone", Self (fun _ -> unset_all language_support_options);
 (* Debugging options *)
-  Exact "-g", Self (fun s -> option_g := true; push_linker_arg s);
+  Exact "-g", Self (fun s -> option_g := true);
 (* Code generation options -- more below *)
   Exact "-O0", Self (fun _ -> unset_all optimization_options);
   Exact "-O", Self (fun _ -> set_all optimization_options);