diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-05-06 12:54:34 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-05-18 14:22:32 +0200 |
| commit | 413bd7681ed70155b7bbc9ab2255801ed41904ea (patch) | |
| tree | f68f78cbdb3c6c81510973f50e7e9a8ac173c0b7 /export | |
| parent | 713b45c5d9e497756a414c049fc255aacc3650c2 (diff) | |
| download | compcert-413bd7681ed70155b7bbc9ab2255801ed41904ea.tar.gz compcert-413bd7681ed70155b7bbc9ab2255801ed41904ea.zip | |
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
Diffstat (limited to 'export')
| -rw-r--r-- | export/ExportDriver.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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 = |