diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-01-03 16:26:14 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-01-03 16:26:14 +0100 |
commit | ca9219d447c37038063f3d297c8f8195bb23e2f1 (patch) | |
tree | e67aee7fa6cea3cbfc242818fd2637e072ce2c02 /driver/Driver.ml | |
parent | 87558f62b29ee94392c3955434aa2680aaaeffa5 (diff) | |
download | compcert-ca9219d447c37038063f3d297c8f8195bb23e2f1.tar.gz compcert-ca9219d447c37038063f3d297c8f8195bb23e2f1.zip |
Remove all temporary files at program exit (#46)
Replaced calls to Filename.temp_file by own version Driveraux.tmp_file.
The Driveraux.tmp_file function takes care that the temporary files are
removed at exit.
Consequently there is no need to explicitly remove temp files in Driver.
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r-- | driver/Driver.ml | 24 |
1 files changed, 6 insertions, 18 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 |