diff --git a/src/kernel_internals/runtime/dump_config.ml b/src/kernel_internals/runtime/dump_config.ml index 09141e5afa0c6302b1bd59548beca9bffbb520a6..32876ff8da8f223b11a792b2593f6cd42adc9b04 100644 --- a/src/kernel_internals/runtime/dump_config.ml +++ b/src/kernel_internals/runtime/dump_config.ml @@ -61,6 +61,9 @@ let dump_to_json () = "framac_libc", `String (Fc_config.framac_libc:>string) ; "plugin_dir", list string (Filepath.Normalized.to_string_list Fc_config.plugin_dir) ; + "lib_dir", `String (Fc_config.libdir:>string) ; + "lib_dirs", + list string (Filepath.Normalized.to_string_list Fc_config.libdirs) ; "preprocessor", `String Fc_config.preprocessor ; "using_default_cpp", `Bool Fc_config.using_default_cpp ; "preprocessor_is_gnu_like", `Bool Fc_config.preprocessor_is_gnu_like ; diff --git a/src/kernel_internals/runtime/fc_config.ml.in b/src/kernel_internals/runtime/fc_config.ml.in index 87f0704a7d164674452601985c9a7af57d8d2443..7da01dcb8df1c887358081bb250f37935a99ea7c 100644 --- a/src/kernel_internals/runtime/fc_config.ml.in +++ b/src/kernel_internals/runtime/fc_config.ml.in @@ -35,6 +35,9 @@ let is_gui = Frama_c_very_first.Gui_init.is_gui let datadirs = (List.map Filepath.Normalized.of_string Config_data.Sites.share) let datadir = List.hd (List.rev datadirs) +let libdirs = (List.map Filepath.Normalized.of_string Config_data.Sites.lib) +let libdir = List.hd (List.rev libdirs) + let plugin_dir = List.map Filepath.Normalized.of_string Config_data.Sites.plugins let plugin_path = diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli index 8be24f24b75a73c5cb65f11bfcad0f42f2a5f4cc..db77f8eac8ca6f95b920dec9ca010d0832d85ccd 100644 --- a/src/kernel_internals/runtime/fc_config.mli +++ b/src/kernel_internals/runtime/fc_config.mli @@ -61,6 +61,15 @@ val framac_libc: Filepath.Normalized.t (** Directory where Frama-C libc headers are. @since 19.0-Potassium *) +val libdirs: Filepath.Normalized.t list +(** Directories where library and executable files are, in order of + priority. + @since Frama-C+dev *) + +val libdir: Filepath.Normalized.t +(** Last directory of libdirs (the directory of frama-c installation) + @since Frama-C+dev *) + val plugin_dir: Filepath.Normalized.t list (** Directory where the Frama-C dynamic plug-ins are. *) diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml index 8aa896f86a21edce59881b558c3f37b67a56d965..ecc8203404c5851a32fa472c1d0f90221b95f444 100644 --- a/src/kernel_internals/runtime/special_hooks.ml +++ b/src/kernel_internals/runtime/special_hooks.ml @@ -31,10 +31,12 @@ let print_config () = "Frama-C %s@\n\ Environment:@\n \ FRAMAC_SHARE = %S@\n \ - FRAMAC_PLUGIN = %S%t@." + FRAMAC_PLUGIN = %S@\n \ + FRAMAC_LIB = %S%t@." Fc_config.version_and_codename (String.concat ":" (Filepath.Normalized.to_string_list Fc_config.datadirs)) (String.concat ":" (Filepath.Normalized.to_string_list Fc_config.plugin_dir)) + (String.concat ":" (Filepath.Normalized.to_string_list Fc_config.libdirs)) (fun fmt -> if Fc_config.preprocessor = "" then Format.fprintf fmt "@\nWarning: no default pre-processor" @@ -67,7 +69,7 @@ let () = Cmdline.run_after_early_stage print_version let print_sharepath = print_configl Kernel.PrintShare.get Fc_config.datadirs let () = Cmdline.run_after_early_stage print_sharepath -let print_libpath = print_configl Kernel.PrintLib.get Fc_config.plugin_dir +let print_libpath = print_configl Kernel.PrintLib.get [Fc_config.libdir] let () = Cmdline.run_after_early_stage print_libpath let print_pluginpath =