From b0a6d8ccfce46c23956e8869ffd0861dbdbd7ef5 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 5 Jul 2024 11:56:31 +0200
Subject: [PATCH] [kernel] Empty pos in Filepath to avoid circular dependancies
---
src/kernel_services/ast_queries/cil_datatype.ml | 7 +------
src/libraries/utils/filepath.ml | 9 +++++++++
src/libraries/utils/filepath.mli | 10 ++++++++++
3 files changed, 20 insertions(+), 6 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index e6eb3769292..15182c27463 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 40ecb41ec45..08bf976d26b 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 9f0e8a8e1b3..3a1a0d43df6 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.
--
GitLab