diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml index e6eb376929273f6cd6b9ca712c98b480611f4e3c..15182c274637ea465bc1bda3f3294c21cacb0912 100644 --- a/src/kernel_services/ast_queries/cil_datatype.ml +++ b/src/kernel_services/ast_queries/cil_datatype.ml @@ -166,12 +166,7 @@ end module Position = struct let pretty_ref = ref UtilsFilepath.pp_pos - let unknown = { - Filepath.pos_path = Datatype.Filepath.dummy; - pos_lnum = 0; - pos_bol = 0; - pos_cnum = -1; - } + let unknown = Filepath.empty_pos let of_lexing_pos p = { Filepath.pos_path = Datatype.Filepath.of_string p.Lexing.pos_fname; pos_lnum = p.Lexing.pos_lnum; diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml index 40ecb41ec45848503214b0b3ab4552066b2d3310..08bf976d26bcf00241e3187ef77d7ca4b809d618 100644 --- a/src/libraries/utils/filepath.ml +++ b/src/libraries/utils/filepath.ml @@ -336,9 +336,18 @@ type position = pos_cnum : int; } +let empty_pos = { + pos_path = Normalized.empty; + pos_lnum = 0; + pos_bol = 0; + pos_cnum = -1; +} + let pp_pos fmt pos = Format.fprintf fmt "%a:%d" Normalized.pretty pos.pos_path pos.pos_lnum +let is_empty_pos pos = pos == empty_pos + let exists (s : Normalized.t) = Sys.file_exists (s :> string) let is_dir (s : Normalized.t) = Sys.is_directory (s :> string) diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli index 9f0e8a8e1b37b8365149968910fd5bfd18a0329a..3a1a0d43df6dd31a18a951fccd74f93c042e66ab 100644 --- a/src/libraries/utils/filepath.mli +++ b/src/libraries/utils/filepath.mli @@ -206,11 +206,21 @@ type position = pos_cnum : int; } +(** Empty position, used as 'dummy' for [Cil_datatype.Position]. + @since Frama-C+dev +*) +val empty_pos : position + (** Pretty-prints a position, in the format file:line. @since 18.0-Argon *) val pp_pos : Format.formatter -> position -> unit +(** Return true if the given position is the empty position. + @since Frama-C+dev +*) +val is_empty_pos : position -> bool + (** Return the current working directory. Implicitly uses {!Unix.realpath} to normalize paths and avoid issues with symbolic links in directory names.