diff options
-rw-r--r-- | cparser/Cprint.ml | 10 | ||||
-rw-r--r-- | cparser/Cprint.mli | 3 | ||||
-rw-r--r-- | driver/Driver.ml | 4 | ||||
-rw-r--r-- | driver/Frontend.ml | 14 |
4 files changed, 18 insertions, 13 deletions
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 0a927873..d623ab96 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -555,3 +555,13 @@ let program pp prog = fprintf pp "@[<v 0>"; List.iter (globdecl pp) prog; fprintf pp "@]@." + +let destination : string option ref = ref None + +let print_if prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out f in + program (formatter_of_out_channel oc) prog; + close_out oc diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli index fe71e4fe..be7ce029 100644 --- a/cparser/Cprint.mli +++ b/cparser/Cprint.mli @@ -33,3 +33,6 @@ val storage : Format.formatter -> C.storage -> unit val field : Format.formatter -> C.field -> unit val globdecl : Format.formatter -> C.globdecl -> unit val program : Format.formatter -> C.program -> unit + +val destination : string option ref +val print_if : C.program -> unit diff --git a/driver/Driver.ml b/driver/Driver.ml index 5afa0a76..b23a4e4f 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -76,7 +76,9 @@ let compile_c_file sourcename ifile ofile = (* Prepare to dump Clight, RTL, etc, if requested *) let set_dest dst opt ext = dst := if !opt then Some (output_filename sourcename ".c" ext) - else None in + else None in + set_dest Cprint.destination option_dparse ".parsed.c"; + set_dest PrintCsyntax.destination option_dcmedium ".compcert.c"; set_dest PrintClight.destination option_dclight ".light.c"; set_dest PrintCminor.destination option_dcminor ".cm"; set_dest PrintRTL.destination option_drtl ".rtl"; diff --git a/driver/Frontend.ml b/driver/Frontend.ml index b4b161b0..148d0f74 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -59,12 +59,7 @@ let parse_c_file sourcename ifile = | None -> exit 2 | Some p -> p 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; + Cprint.print_if ast; (* Conversion to Csyntax *) let csyntax = match Timing.time "CompCert C generation" C2C.convertProgram ast with @@ -72,12 +67,7 @@ let parse_c_file sourcename ifile = | Some p -> p in flush stderr; (* Save CompCert C AST if requested *) - if !option_dcmedium then begin - let ofile = output_filename sourcename ".c" ".compcert.c" in - let oc = open_out ofile in - PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; - close_out oc - end; + PrintCsyntax.print_if csyntax; csyntax (* Add gnu preprocessor list *) |