From e4d2045edde7d8f8a94a903a3ea48cec6c582544 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 16 Nov 2020 11:49:40 +0100
Subject: [PATCH] [Filepath] add special_stdout notation (-)
---
src/libraries/utils/filepath.ml | 11 +++++++++--
src/libraries/utils/filepath.mli | 5 +++++
2 files changed, 14 insertions(+), 2 deletions(-)
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 20ea5cc4886..76e2b687498 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -267,10 +267,17 @@ module Normalized = struct
if case_sensitive then String.compare s1 s2
else Extlib.compare_ignore_case s1 s2
- let pretty fmt p = Format.fprintf fmt "%s" (pretty p)
- let pp_abs fmt p = Format.fprintf fmt "%s" p
let unknown = normalize ""
let is_unknown fp = equal fp unknown
+ let special_stdout = normalize "-"
+ let is_special_stdout fp = equal fp special_stdout
+
+ let pretty fmt p =
+ if is_special_stdout p then
+ Format.fprintf fmt "<stdout>"
+ else
+ Format.fprintf fmt "%s" (pretty p)
+ let pp_abs fmt p = Format.fprintf fmt "%s" p
let is_file fp =
try
(Unix.stat (fp :> string)).Unix.st_kind = Unix.S_REG
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index e2958f5edda..79a3d7fad11 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -156,6 +156,11 @@ module Normalized: sig
(** @since 20.0-Calcium *)
val is_unknown: t -> bool
+ (** [is_special_stdout f] returns [true] iff [f] is '-' (a single dash),
+ which is a special notation for 'stdout'.
+ @since Frama-C+dev *)
+ val is_special_stdout: 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.
--
GitLab