aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml25
1 files changed, 13 insertions, 12 deletions
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);