diff options
| -rw-r--r-- | driver/Driver.ml | 24 | ||||
| -rw-r--r-- | driver/Driveraux.ml | 5 | ||||
| -rw-r--r-- | driver/Driveraux.mli | 5 | ||||
| -rw-r--r-- | exportclight/Clightgen.ml | 2 |
4 files changed, 17 insertions, 19 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 21fb0db3..55d06833 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -67,11 +67,8 @@ let dump_jasm asm sourcename destfile = let object_filename sourcename suff = if nolink () then output_filename ~final: !option_c sourcename suff ".o" - else begin - let tmpfile = Filename.temp_file "compcert" ".o" in - at_exit (fun () -> safe_remove tmpfile); - tmpfile - end + else + tmp_file ".o" (* From CompCert C AST to asm *) @@ -125,33 +122,26 @@ let process_c_file sourcename = let preproname = if !option_dprepro then output_filename sourcename ".c" ".i" else - Filename.temp_file "compcert" ".i" in + tmp_file ".i" in preprocess sourcename preproname; let name = if !option_interp then begin Machine.config := Machine.compcert_interpreter !Machine.config; let csyntax = parse_c_file sourcename preproname in - if not !option_dprepro then - safe_remove preproname; Interp.execute csyntax; "" end else if !option_S then begin compile_c_file sourcename preproname (output_filename ~final:true sourcename ".c" ".s"); - if not !option_dprepro then - safe_remove preproname; "" end else begin let asmname = if !option_dasm then output_filename sourcename ".c" ".s" - else Filename.temp_file "compcert" ".s" in + else tmp_file ".s" in compile_c_file sourcename preproname asmname; - if not !option_dprepro then - safe_remove preproname; let objname = object_filename sourcename ".c" in assemble asmname objname; - if not !option_dasm then safe_remove asmname; objname end in name @@ -173,11 +163,10 @@ let process_i_file sourcename = let asmname = if !option_dasm then output_filename sourcename ".c" ".s" - else Filename.temp_file "compcert" ".s" in + else tmp_file ".s" in compile_c_file sourcename sourcename asmname; let objname = object_filename sourcename ".c" in assemble asmname objname; - if not !option_dasm then safe_remove asmname; objname end @@ -196,11 +185,10 @@ let process_S_file sourcename = preprocess sourcename (output_filename_default "-"); "" end else begin - let preproname = Filename.temp_file "compcert" ".s" in + let preproname = tmp_file ".s" in preprocess sourcename preproname; let objname = object_filename sourcename ".S" in assemble preproname objname; - safe_remove preproname; objname end diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 2c478fb1..6d8d0adc 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -18,6 +18,11 @@ open Clflags let safe_remove file = try Sys.remove file with Sys_error _ -> () +let tmp_file suff = + let tmpfile = Filename.temp_file "compcert" suff in + at_exit (fun () -> safe_remove tmpfile); + tmpfile + (* Invocation of external tools *) let rec waitpid_no_intr pid = diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 274ecedd..51333b2a 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -22,6 +22,11 @@ val command_error: string -> int -> unit val safe_remove: string -> unit (** Remove the given file if it exists *) +val tmp_file: string -> string + (** Create a temporary file with the given suffix. + The file will be removed when the program exits. + Return the absolute path to the file. *) + val output_filename: ?final:bool -> string -> string -> string -> string (** Determine names for output files. We use -o option if specified and if this is the final destination file (not a dump file). diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index ae1d09a6..05ece5de 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -69,7 +69,7 @@ let process_c_file sourcename = if !option_E then begin preprocess sourcename "-" end else begin - let preproname = Filename.temp_file "compcert" ".i" in + let preproname = Driveraux.tmp_file ".i" in preprocess sourcename preproname; compile_c_file sourcename preproname (prefixname ^ ".v") end |