diff options
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r-- | driver/Driver.ml | 25 |
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); |