diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml index d20cc20285af3175eabfb4202058616734e426ae..7751148395679839085c4989ae468f40c186133b 100644 --- a/src/kernel_services/cmdline_parameters/parameter_builder.ml +++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml @@ -483,7 +483,12 @@ struct let newfp = Filepath.Normalized.to_pretty_string newstr in f oldfp newfp - let set fp = check_existence existence fp ; set fp + let set fp = + try + check_existence existence fp ; set fp + with + | No_file -> P.L.abort "file not found: '%a'" Filepath.Normalized.pretty fp + | File_exists -> P.L.abort "file already exists: '%a'" Filepath.Normalized.pretty fp let set_str s = set (Filepath.Normalized.of_string s) diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli index a36076d68471974e040e4d0cebef792d3d185d74..880334713ba96b5682923dd9d36af239d0214d07 100644 --- a/src/kernel_services/cmdline_parameters/parameter_sig.mli +++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli @@ -327,14 +327,17 @@ type existence = Must_exist | Must_not_exist | Indifferent module type Filepath = sig exception No_file - (** raised by {!set} if no file exists and [existence] is [Must_exist]. *) + (** raised by {!check_existence} if no file exists and [existence] is [Must_exist]. *) exception File_exists - (** raised by {!set} if some file exists and [existence] is + (** raised by {!check_existence} if some file exists and [existence] is [Must_nos_exist]. *) val existence: existence + val check_existence: existence -> Filepath.Normalized.t -> unit + (** Checks the existence/absence of a file. May raise [No_file] or [File_exists]. *) + include S with type t = Filepath.Normalized.t end diff --git a/tests/misc/filepath.i b/tests/misc/filepath.i index f5c0183704fb0f14aba28d804eb133137365c870..a8892bc2d2feb203e5bef30c636a78b7d481c254 100644 --- a/tests/misc/filepath.i +++ b/tests/misc/filepath.i @@ -1,4 +1,5 @@ /* run.config - EXECNOW: make -s @PTEST_DIR@/filepath_test.cmxs - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/filepath_test + MODULE: tests/misc/filepath_test.cmxs + COMMENT: the '-load' option below intentionally contains an error + OPT: -no-autoload-plugins -load nonexistent_file.sav */ diff --git a/tests/misc/oracle/filepath.res.oracle b/tests/misc/oracle/filepath.res.oracle index 2efe6c776421c1f7ee60b7dfe9fb4c5840a8075c..51185cac23a1a9a37d548d9d820267990e03d934 100644 --- a/tests/misc/oracle/filepath.res.oracle +++ b/tests/misc/oracle/filepath.res.oracle @@ -9,4 +9,5 @@ [kernel] relativize(.): . [kernel] relativize(./tests/..): . [kernel] relativize(/a/bc/d,base_name:/a/b/): /a/bc/d -[kernel] Parsing tests/misc/filepath.i (no preprocessing) +[kernel] User Error: file not found: 'nonexistent_file.sav' +[kernel] Frama-C aborted: invalid user input.