From c41ac97722fbc2155d0514f3e02dc195850b87f5 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 2 Sep 2020 10:21:23 +0200
Subject: [PATCH] [Filepath] add Filepath.Normalized.is_file

---
 src/libraries/utils/filepath.ml  | 4 ++++
 src/libraries/utils/filepath.mli | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 4e5a859748c..4e02418356f 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 39c084bffa8..41c56ec8167 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.
-- 
GitLab