Merge branch 'fix/andre/filepath-no-exist' into 'master'

[Kernel] better handling of non-existing filepaths

Closes #741

See merge request frama-c/frama-c!2441

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)
 

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

tests/misc/filepath.i

 /* 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
  */

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.