From ca9219d447c37038063f3d297c8f8195bb23e2f1 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bschommer@users.noreply.github.com>
Date: Wed, 3 Jan 2018 16:26:14 +0100
Subject: 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.
---
 driver/Driver.ml          | 24 ++++++------------------
 driver/Driveraux.ml       |  5 +++++
 driver/Driveraux.mli      |  5 +++++
 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
-- 
cgit