diff options
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index d22dd77c..80a5891c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -15,6 +15,7 @@ open Commandline open Camlcoq open Clflags open Timing +open CtoDwarf (* Location of the compatibility library *) @@ -128,6 +129,9 @@ let parse_c_file sourcename ifile = Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc end; + let debug = if !option_g && Configuration.advanced_debug then + Some (program_to_dwarf ast sourcename) + else None in (* Conversion to Csyntax *) let csyntax = match Timing.time "CompCert C generation" C2C.convertProgram ast with @@ -141,7 +145,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 +161,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 +185,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 +217,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" @@ -265,7 +270,7 @@ let process_c_file sourcename = let preproname = Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; if !option_interp then begin - let csyntax = parse_c_file sourcename preproname in + let csyntax,_ = parse_c_file sourcename preproname in safe_remove preproname; Interp.execute csyntax; "" @@ -292,7 +297,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 @@ -509,7 +514,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); |