diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml index 4e5a859748ce24d79b52a441a180bfe9b23d351f..4e02418356f54681e995a49fb8bb5a9baca1d319 100644 --- a/src/libraries/utils/filepath.ml +++ b/src/libraries/utils/filepath.ml @@ -252,6 +252,10 @@ module Normalized = struct let pp_abs fmt p = Format.fprintf fmt "%s" p let unknown = normalize "" let is_unknown fp = equal fp unknown + let is_file fp = + try + (Unix.stat (fp :> string)).Unix.st_kind = Unix.S_REG + with _ -> false end type position = diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli index 39c084bffa8cecef1fb71baca36e9870c5d834c1..41c56ec816717618e136353f659045276feadad5 100644 --- a/src/libraries/utils/filepath.mli +++ b/src/libraries/utils/filepath.mli @@ -144,6 +144,12 @@ module Normalized: sig (** @since 20.0-Calcium *) val is_unknown: t -> bool + + (** [is_file f] returns [true] iff [f] points to a regular file + (or a symbolic link pointing to a file). + Returns [false] if any errors happen when [stat]'ing the file. + @since Frama-C+dev *) + val is_file: t -> bool end (** Describes a position in a source file.