Simplify handling of file suffixes.

Since we are sure that all files passed have a valid extension we can
use the OCaml function Filename.remove_extension and don't need to pass
the suffixes.
Bug 33218

4 files changed, 28 insertions, 30 deletions

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 0686f193..4266e57e 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -30,18 +30,18 @@ let sdump_suffix = ref ".json"
 let nolink () =
   !option_c || !option_S || !option_E || !option_interp
 
-let object_filename sourcename suff =
+let object_filename sourcename =
   if nolink () then
-    output_filename ~final: !option_c sourcename suff ".o"
+    output_filename ~final: !option_c sourcename ~suffix:".o"
   else
     tmp_file ".o"
 
 (* From CompCert C AST to asm *)
 
-let compile_c_file sourcename ~sourcesuffix ifile ofile =
+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 sourcesuffix ext)
+    dst := if !opt then Some (output_filename sourcename ~suffix:ext)
       else None in
   set_dest Cprint.destination option_dparse ".parsed.c";
   set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
@@ -73,23 +73,23 @@ let compile_c_file sourcename ~sourcesuffix ifile ofile =
 
 (* From C source to asm *)
 
-let compile_i_file sourcename ~sourcesuffix preproname =
+let compile_i_file sourcename preproname =
   if !option_interp then begin
     Machine.config := Machine.compcert_interpreter !Machine.config;
     let csyntax = parse_c_file sourcename preproname in
     Interp.execute csyntax;
         ""
   end else if !option_S then begin
-    compile_c_file sourcename ~sourcesuffix:sourcesuffix preproname
-      (output_filename ~final:true sourcename sourcesuffix ".s");
+    compile_c_file sourcename preproname
+      (output_filename ~final:true sourcename ~suffix:".s");
     ""
   end else begin
     let asmname =
       if !option_dasm
-      then output_filename sourcename sourcesuffix ".s"
+      then output_filename sourcename ~suffix:".s"
       else tmp_file ".s" in
-    compile_c_file sourcename ~sourcesuffix:sourcesuffix preproname asmname;
-    let objname = object_filename sourcename sourcesuffix in
+    compile_c_file sourcename preproname asmname;
+    let objname = object_filename sourcename  in
     assemble asmname objname;
     objname
   end
@@ -103,24 +103,24 @@ let process_c_file sourcename =
     ""
   end else begin
     let preproname = if !option_dprepro then
-      output_filename sourcename ".c" ".i"
+      output_filename sourcename ~suffix:".i"
     else
       tmp_file ".i" in
     preprocess sourcename preproname;
-    compile_i_file sourcename ~sourcesuffix:".c" preproname
+    compile_i_file sourcename preproname
   end
 
 (* Processing of a .i / .p file (preprocessed C) *)
 
-let process_i_file sourcename ~sourcesuffix =
+let process_i_file sourcename =
   ensure_inputfile_exists sourcename;
-  compile_i_file sourcename ~sourcesuffix:sourcesuffix sourcename
+  compile_i_file sourcename sourcename
 
 (* Processing of .S and .s files *)
 
 let process_s_file sourcename =
   ensure_inputfile_exists sourcename;
-  let objname = object_filename sourcename ".s" in
+  let objname = object_filename sourcename in
   assemble sourcename objname;
   objname
 
@@ -132,7 +132,7 @@ let process_S_file sourcename =
   end else begin
     let preproname = tmp_file ".s" in
     preprocess sourcename preproname;
-    let objname = object_filename sourcename ".S" in
+    let objname = object_filename sourcename in
     assemble preproname objname;
     objname
   end
@@ -379,11 +379,9 @@ let cmdline_actions =
   Suffix ".c", Self (fun s ->
       push_action process_c_file s; incr num_source_files; incr num_input_files);
   Suffix ".i", Self (fun s ->
-      push_action (process_i_file ~sourcesuffix:".i") s;
-      incr num_source_files; incr num_input_files);
+      push_action process_i_file s; incr num_source_files; incr num_input_files);
   Suffix ".p", Self (fun s ->
-      push_action (process_i_file ~sourcesuffix:".p") s;
-      incr num_source_files; incr num_input_files);
+      push_action process_i_file s; incr num_source_files; incr num_input_files);
   Suffix ".s", Self (fun s ->
       push_action process_s_file s; incr num_source_files; incr num_input_files);
   Suffix ".S", Self (fun s ->
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index 5b2d792e..4b9809a6 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -89,12 +89,12 @@ let command_error n exc =
    and if this is the final destination file (not a dump file).
    Otherwise, we generate a file in the current directory. *)
 
-let output_filename ?(final = false) source_file source_suffix output_suffix =
+let output_filename ?(final = false) source_file ~suffix =
   match !option_o with
   | Some file when final -> file
   | _ ->
-    Filename.basename (Filename.chop_suffix source_file source_suffix)
-    ^ output_suffix
+    Filename.basename (Filename.remove_extension source_file)
+    ^ suffix
 
 (* A variant of [output_filename] where the default output name is fixed *)
 
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli
index 6f0eaddb..47f923f0 100644
--- a/driver/Driveraux.mli
+++ b/driver/Driveraux.mli
@@ -27,7 +27,7 @@ val tmp_file: string -> string
        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
+val output_filename: ?final:bool -> string -> suffix: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).
        Otherwise, we generate a file in the current directory. *)
diff --git a/export/ExportDriver.ml b/export/ExportDriver.ml
index d7980994..365392c3 100644
--- a/export/ExportDriver.ml
+++ b/export/ExportDriver.ml
@@ -67,7 +67,7 @@ let export_clight sourcename csyntax ofile =
 
 let compile_c_file sourcename ifile ofile =
   let set_dest dst opt ext =
-    dst := if !opt then Some (output_filename sourcename ".c" ext)
+    dst := if !opt then Some (output_filename sourcename ~suffix:ext)
       else None in
   set_dest Cprint.destination option_dparse ".parsed.c";
   set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
@@ -77,20 +77,20 @@ let compile_c_file sourcename ifile ofile =
   | Mode_Csyntax -> export_csyntax sourcename cs ofile
   | Mode_Clight  -> export_clight sourcename cs ofile
 
-let output_filename sourcename suff =
-  let prefixname = Filename.chop_suffix sourcename suff in
+let output_filename sourcename  =
+  let prefixname = Filename.remove_extension sourcename in
   output_filename_default (prefixname ^ ".v")
 
 (* Processing of a .c file *)
 
 let process_c_file sourcename =
   ensure_inputfile_exists sourcename;
-  let ofile = output_filename sourcename ".c" in
+  let ofile = output_filename sourcename in
   if !option_E then begin
     preprocess sourcename "-"
   end else begin
     let preproname = if !option_dprepro then
-        Driveraux.output_filename sourcename ".c" ".i"
+        Driveraux.output_filename sourcename ~suffix:".i"
       else
         Driveraux.tmp_file ".i" in
     preprocess sourcename preproname;
@@ -101,7 +101,7 @@ let process_c_file sourcename =
 
 let process_i_file sourcename =
   ensure_inputfile_exists sourcename;
-  let ofile = output_filename sourcename ".i" in
+  let ofile = output_filename sourcename in
   compile_c_file sourcename sourcename ofile
 
 let usage_string =