From 57b73127110cbba1013d428cacf17c3aafdee674 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 5 Apr 2024 14:07:40 +0200
Subject: [PATCH] [kernel] introduce paths in system_config
---
src/kernel_internals/runtime/special_hooks.ml | 6 +++---
src/kernel_internals/runtime/system_config.ml.in | 2 ++
src/kernel_internals/runtime/system_config.mli | 8 +++++++-
3 files changed, 12 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 79eca6bb93..d888e02671 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -34,9 +34,9 @@ let print_config () =
FRAMAC_PLUGIN = %S@\n \
FRAMAC_LIB = %S%t@."
System_config.Version.id_and_codename
- (String.concat ":" (Filepath.Normalized.to_string_list System_config.Share.dirs))
- (String.concat ":" (Filepath.Normalized.to_string_list System_config.Plugins.dirs))
- (String.concat ":" (Filepath.Normalized.to_string_list System_config.Lib.dirs))
+ (System_config.Share.path)
+ (System_config.Plugins.path)
+ (System_config.Lib.path)
(fun fmt ->
if System_config.Preprocessor.command = "" then
Format.fprintf fmt "@\nWarning: no default preprocessor"
diff --git a/src/kernel_internals/runtime/system_config.ml.in b/src/kernel_internals/runtime/system_config.ml.in
index 82f9d83e49..fbf4944d65 100644
--- a/src/kernel_internals/runtime/system_config.ml.in
+++ b/src/kernel_internals/runtime/system_config.ml.in
@@ -34,6 +34,7 @@ let is_gui = Frama_c_very_first.Gui_init.is_gui
module Share = struct
let dirs = List.map Filepath.Normalized.of_string Config_data.Sites.share
+ let path = String.concat ":" (Filepath.Normalized.to_string_list dirs)
let main = List.hd (List.rev dirs)
let libc = Filepath.Normalized.concat main "libc"
@@ -42,6 +43,7 @@ end
module Lib = struct
let dirs = List.map Filepath.Normalized.of_string Config_data.Sites.lib
+ let path = String.concat ":" (Filepath.Normalized.to_string_list dirs)
let main = List.hd (List.rev dirs)
end
diff --git a/src/kernel_internals/runtime/system_config.mli b/src/kernel_internals/runtime/system_config.mli
index c04d17ec90..ccceae3922 100644
--- a/src/kernel_internals/runtime/system_config.mli
+++ b/src/kernel_internals/runtime/system_config.mli
@@ -48,6 +48,9 @@ module Share : sig
val main: Filepath.Normalized.t
(** Last directory of dirs (the directory of frama-c installation) *)
+ val path: string
+ (** The colon-separated concatenation of {!dirs}. *)
+
val libc: Filepath.Normalized.t
(** Directory where Frama-C libc headers are. *)
end
@@ -57,6 +60,9 @@ module Lib : sig
(** Directories where library and executable files are, in order of
priority. *)
+ val path: string
+ (** The colon-separated concatenation of {!dirs}. *)
+
val main: Filepath.Normalized.t
(** Last directory of libdirs (the directory of frama-c installation) *)
end
@@ -66,7 +72,7 @@ module Plugins : sig
(** Directories where the Frama-C dynamic plug-ins are. *)
val path: string
- (** The colon-separated concatenation of [plugin_dir]. *)
+ (** The colon-separated concatenation of {!dirs}. *)
val load: string -> unit
(** Load given plug-in name *)
--
GitLab