diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-01-04 18:35:40 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-01-04 18:35:40 +0100 |
| commit | 8219490aae44fa79932d913cc69941d6b22a70a3 (patch) | |
| tree | b60527a283191e2293a4af3497e48303402ee626 /driver/Frontend.ml | |
| parent | b1455cc40ebf6bb00722ff128e702f83c9b4dca8 (diff) | |
| download | compcert-kvx-8219490aae44fa79932d913cc69941d6b22a70a3.tar.gz compcert-kvx-8219490aae44fa79932d913cc69941d6b22a70a3.zip | |
Handle dcompcertc and dparsedc like all dump opts.
This time with the correct place for setting the destination files.
Bug 20521
Diffstat (limited to 'driver/Frontend.ml')
| -rw-r--r-- | driver/Frontend.ml | 14 |
1 files changed, 2 insertions, 12 deletions
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 *) |