diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml index 2d78d5983034c8de67c10c1a1a9d5d5c5f5ee19f..a9719dc39c36377dff12a0bf43e6c0d4a6cbd232 100644 --- a/src/libraries/utils/filepath.ml +++ b/src/libraries/utils/filepath.ml @@ -224,6 +224,7 @@ module Normalized = struct 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 end type position = diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli index 5825faaf39666c6e7fa0cfb130c33dae5333797b..2afff02a14dece4316164ba48727895002f224bf 100644 --- a/src/libraries/utils/filepath.mli +++ b/src/libraries/utils/filepath.mli @@ -120,6 +120,9 @@ module Normalized: sig (** Unknown filepath, used as 'dummy' for [Datatype.Filepath]. *) val unknown: t + + (** @since Frama-C+dev *) + val is_unknown: t -> bool end (** Describes a position in a source file.