diff --git a/share/analysis-scripts/list_functions.ml b/share/analysis-scripts/list_functions.ml
index 022fdb66fec8ad54856275ee6088eff468094d90..b497e3d40021de949465780237455d794213b3f7 100644
--- a/share/analysis-scripts/list_functions.ml
+++ b/share/analysis-scripts/list_functions.ml
@@ -115,7 +115,7 @@ class stmt_count_visitor =
location-based approach. *)
let located_within_framac_libc loc =
let pos = fst loc in
- Filepath.is_relative ~base_name:System_config.framac_libc pos.Filepath.pos_path
+ Filepath.is_relative ~base_name:System_config.Share.libc pos.Filepath.pos_path
class fun_cabs_visitor print_libc = object(self)
inherit Cabsvisit.nopCabsVisitor
diff --git a/src/init/toplevel/toplevel_config.ml b/src/init/toplevel/toplevel_config.ml
index 4c9e99e129b6d4e2acd641ff9beab10975556d17..9638c5d82a46847ff0d16802c578914dd9e7dbd2 100644
--- a/src/init/toplevel/toplevel_config.ml
+++ b/src/init/toplevel/toplevel_config.ml
@@ -20,4 +20,4 @@
(* *)
(**************************************************************************)
-let () = Topdirs.dir_directory System_config.libdir
+let () = Topdirs.dir_directory System_config.Lib.main
diff --git a/src/kernel_internals/runtime/dump_config.ml b/src/kernel_internals/runtime/dump_config.ml
index aa533fa3e9776256e1d418c98f7a70a3ccd6b6e5..2e5727d948e4e5f1382a5fc0b753d72fff2d7eee 100644
--- a/src/kernel_internals/runtime/dump_config.ml
+++ b/src/kernel_internals/runtime/dump_config.ml
@@ -45,31 +45,31 @@ let dump_to_json () =
let string s = `String s in
let list f l = `List (List.map f l) in
`Assoc [
- "version", `String System_config.version ;
- "codename", `String System_config.codename ;
- "version_and_codename", `String System_config.version_and_codename ;
- "major_version", `Int System_config.major_version ;
- "minor_version", `Int System_config.minor_version ;
+ "version", `String System_config.Version.id ;
+ "codename", `String System_config.Version.codename ;
+ "version_and_codename", `String System_config.Version.id_and_codename ;
+ "major_version", `Int System_config.Version.major ;
+ "minor_version", `Int System_config.Version.minor ;
"is_gui", `Bool System_config.is_gui ;
(* "lablgtk", `String System_config.lablgtk ;
* "ocamlc", `String System_config.ocamlc ;
* "ocamlopt", `String System_config.ocamlopt ;
* "ocaml_wflags", `String System_config.ocaml_wflags ; *)
- "datadir", `String (System_config.datadir:>string) ;
+ "datadir", `String (System_config.Share.main:>string) ;
"datadirs",
- list string (Filepath.Normalized.to_string_list System_config.datadirs) ;
- "framac_libc", `String (System_config.framac_libc:>string) ;
+ list string (Filepath.Normalized.to_string_list System_config.Share.dirs) ;
+ "framac_libc", `String (System_config.Share.libc:>string) ;
"plugin_dir",
- list string (Filepath.Normalized.to_string_list System_config.plugin_dir) ;
- "lib_dir", `String (System_config.libdir:>string) ;
+ list string (Filepath.Normalized.to_string_list System_config.Plugins.dirs) ;
+ "lib_dir", `String (System_config.Lib.main:>string) ;
"lib_dirs",
- list string (Filepath.Normalized.to_string_list System_config.libdirs) ;
- "preprocessor", `String System_config.preprocessor ;
- "using_default_cpp", `Bool System_config.using_default_cpp ;
- "preprocessor_is_gnu_like", `Bool System_config.preprocessor_is_gnu_like ;
+ list string (Filepath.Normalized.to_string_list System_config.Lib.dirs) ;
+ "preprocessor", `String System_config.Preprocessor.command ;
+ "using_default_cpp", `Bool System_config.Preprocessor.is_default ;
+ "preprocessor_is_gnu_like", `Bool System_config.Preprocessor.is_gnu_like ;
"preprocessor_supported_arch_options",
- list string System_config.preprocessor_supported_arch_options ;
- "preprocessor_keep_comments", `Bool System_config.preprocessor_keep_comments ;
+ list string System_config.Preprocessor.supported_arch_options ;
+ "preprocessor_keep_comments", `Bool System_config.Preprocessor.keep_comments ;
"current_machdep", `String (Kernel.Machdep.get ()) ;
"machdeps", list string (File.list_available_machdeps ()) ;
"plugins", list string (list_plugin_names ()) ;
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 2452683347c3e0f7bbb6d03eb692d8f981fb34c8..79eca6bb935bf88d83c619c7d2f5bc36d4c9c949 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -33,14 +33,14 @@ let print_config () =
FRAMAC_SHARE = %S@\n \
FRAMAC_PLUGIN = %S@\n \
FRAMAC_LIB = %S%t@."
- System_config.version_and_codename
- (String.concat ":" (Filepath.Normalized.to_string_list System_config.datadirs))
- (String.concat ":" (Filepath.Normalized.to_string_list System_config.plugin_dir))
- (String.concat ":" (Filepath.Normalized.to_string_list System_config.libdirs))
+ 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))
(fun fmt ->
- if System_config.preprocessor = "" then
+ if System_config.Preprocessor.command = "" then
Format.fprintf fmt "@\nWarning: no default preprocessor"
- else if not System_config.preprocessor_keep_comments then
+ else if not System_config.Preprocessor.keep_comments then
Format.fprintf fmt
"@\nWarning: default preprocessor is not able to keep comments \
(hence ACSL annotations) in its output")
@@ -66,21 +66,21 @@ let print_configl get value () =
end
let print_version =
- print_config Kernel.PrintVersion.get System_config.version_and_codename
+ print_config Kernel.PrintVersion.get System_config.Version.id_and_codename
let () = Cmdline.run_after_early_stage print_version
let print_version_newline =
- print_config ~newline:true Kernel.Version.get System_config.version_and_codename
+ print_config ~newline:true Kernel.Version.get System_config.Version.id_and_codename
let () = Cmdline.run_after_early_stage print_version_newline
-let print_sharepath = print_configl Kernel.PrintShare.get System_config.datadirs
+let print_sharepath = print_configl Kernel.PrintShare.get System_config.Share.dirs
let () = Cmdline.run_after_early_stage print_sharepath
-let print_libpath = print_configl Kernel.PrintLib.get [System_config.libdir]
+let print_libpath = print_configl Kernel.PrintLib.get [System_config.Lib.main]
let () = Cmdline.run_after_early_stage print_libpath
let print_pluginpath =
- print_config Kernel.PrintPluginPath.get System_config.plugin_path
+ print_config Kernel.PrintPluginPath.get System_config.Plugins.path
let () = Cmdline.run_after_early_stage print_pluginpath
(**************************************************************************)
diff --git a/src/kernel_internals/runtime/system_config.ml.in b/src/kernel_internals/runtime/system_config.ml.in
index 527d63404860fc2e8156e2d263a20981b1ecea09..9f577e1c294319d7d59e707b4b6c218c3e162fc7 100644
--- a/src/kernel_internals/runtime/system_config.ml.in
+++ b/src/kernel_internals/runtime/system_config.ml.in
@@ -22,56 +22,63 @@
# 24 "src/kernel_internals/runtime/system_config.ml.in"
-let version = "@VERSION@"
-let codename = "@VERSION_CODENAME@"
-let version_and_codename = version ^ " (" ^ codename ^ ")"
-
-let major_version = @MAJOR_VERSION@
-
-let minor_version = @MINOR_VERSION@
+module Version = struct
+ let id = "@VERSION@"
+ let codename = "@VERSION_CODENAME@"
+ let id_and_codename = id ^ " (" ^ codename ^ ")"
+ let major = @MAJOR_VERSION@
+ let minor = @MINOR_VERSION@
+end
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)
+module Share = struct
+ let dirs = List.map Filepath.Normalized.of_string Config_data.Sites.share
+ let main = List.hd (List.rev dirs)
+ let libc = Filepath.Normalized.concat main "libc"
-let plugin_dir = List.map Filepath.Normalized.of_string Config_data.Sites.plugins
+ let () = Filepath.add_symbolic_dir_list "FRAMAC_SHARE" dirs
+end
-let plugin_path =
- String.concat ":" (Filepath.Normalized.to_string_list plugin_dir)
+module Lib = struct
+ let dirs = List.map Filepath.Normalized.of_string Config_data.Sites.lib
+ let main = List.hd (List.rev dirs)
+end
-let framac_libc = Filepath.Normalized.concat datadir "libc"
+module Plugins = struct
+ let dirs = List.map Filepath.Normalized.of_string Config_data.Sites.plugins
+ let path = String.concat ":" (Filepath.Normalized.to_string_list dirs)
-let () = Filepath.add_symbolic_dir_list "FRAMAC_SHARE" datadirs
-let () = Filepath.add_symbolic_dir_list "FRAMAC_PLUGIN" plugin_dir
+ let () = Filepath.add_symbolic_dir_list "FRAMAC_PLUGIN" dirs
+end
-let default_cpp = "@FRAMAC_DEFAULT_CPP@"
+module Preprocessor = struct
+ let default = "@FRAMAC_DEFAULT_CPP@"
-let default_cpp_args = " @FRAMAC_DEFAULT_CPP_ARGS@"
+ let default_args = " @FRAMAC_DEFAULT_CPP_ARGS@"
-let env_or_default f vdefault =
- try
- let env = Sys.getenv "CPP" ^ default_cpp_args in
- if env=default_cpp then vdefault else f env
- with Not_found -> vdefault
+ let env_or_default f vdefault =
+ try
+ let env = Sys.getenv "CPP" ^ default_args in
+ if env = default then vdefault else f env
+ with Not_found -> vdefault
-let preprocessor = env_or_default (fun x -> x) default_cpp
+ let command = env_or_default (fun x -> x) default
-let using_default_cpp = env_or_default (fun _ -> false) true
+ let is_default = env_or_default (fun _ -> false) true
-let preprocessor_is_gnu_like =
- env_or_default
- (fun _ ->
- (* be more lenient when trying to determine if the preprocessor
- is gnu-like: in Cygwin, for instance, CC is "<prefix>-gcc" but
- CPP is "<prefix>-cpp", so this extra test allows proper detection. *)
- let env = Sys.getenv "CC" ^ default_cpp_args in
- env=default_cpp) @FRAMAC_GNU_CPP@
+ let is_gnu_like =
+ env_or_default
+ (fun _ ->
+ (* be more lenient when trying to determine if the preprocessor
+ is gnu-like: in Cygwin, for instance, CC is "<prefix>-gcc" but
+ CPP is "<prefix>-cpp", so this extra test allows proper detection.
+ *)
+ let env = Sys.getenv "CC" ^ default_args in
+ env=default) @FRAMAC_GNU_CPP@
-let preprocessor_supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@]
+ let keep_comments =
+ env_or_default (fun _ -> true) @DEFAULT_CPP_KEEP_COMMENTS@
-let preprocessor_keep_comments =
- env_or_default (fun _ -> true) @DEFAULT_CPP_KEEP_COMMENTS@
+ let supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@]
+end
diff --git a/src/kernel_internals/runtime/system_config.mli b/src/kernel_internals/runtime/system_config.mli
index fe303eec5779ce977d9221abc22cf5a7f18992b8..5cd197220db17c0684508f7ce98de24f62d752fa 100644
--- a/src/kernel_internals/runtime/system_config.mli
+++ b/src/kernel_internals/runtime/system_config.mli
@@ -20,27 +20,85 @@
(* *)
(**************************************************************************)
-(** Information about version of Frama-C.
- The body of this module is generated from Makefile. *)
-
-val version: string
-(** Frama-C Version identifier. *)
-
-val codename: string
-(** Frama-C version codename.
- @since 18.0-Argon *)
-
-val version_and_codename: string
-(** Frama-C version and codename.
- @since 18.0-Argon *)
-
-val major_version: int
-(** Frama-C major version number.
- @since 19.0-Potassium *)
-
-val minor_version: int
-(** Frama-C minor version number.
- @since 19.0-Potassium *)
+(** Information about the enrivonment *)
+
+module Version : sig
+ val id: string
+ (** Frama-C Version identifier. *)
+
+ val codename: string
+ (** Frama-C version codename. *)
+
+ val id_and_codename: string
+ (** Frama-C version and codename. *)
+
+ val major: int
+ (** Frama-C major version number. *)
+
+ val minor: int
+ (** Frama-C minor version number. *)
+end
+
+module Share : sig
+ val dirs: Filepath.Normalized.t list
+ (** Directories where architecture independent files are in order of
+ priority.
+ *)
+
+ val main: Filepath.Normalized.t
+ (** Last directory of dirs (the directory of frama-c installation) *)
+
+ val libc: Filepath.Normalized.t
+ (** Directory where Frama-C libc headers are. *)
+end
+
+module Lib : sig
+ val dirs: Filepath.Normalized.t list
+ (** Directories where library and executable files are, in order of
+ priority. *)
+
+ val main: Filepath.Normalized.t
+ (** Last directory of libdirs (the directory of frama-c installation) *)
+end
+
+module Plugins : sig
+ val dirs: Filepath.Normalized.t list
+ (** Directories where the Frama-C dynamic plug-ins are. *)
+
+ val path: string
+ (** The colon-separated concatenation of [plugin_dir]. *)
+end
+
+module Preprocessor : sig
+ val command: string
+ (** Name of the default command to call the preprocessor.
+ If the CPP environment variable is set, use it
+ else use the built-in default from autoconf. Usually this is
+ "gcc -C -E -I."
+ *)
+
+ val is_default: bool
+ (** whether the preprocessor command is the one defined at configure time
+ or the result of taking a CPP environment variable, in case it differs
+ *)
+
+ val is_gnu_like: bool
+ (** whether the default preprocessor accepts the same options as gcc
+ (i.e. is either gcc or clang), when this is the case, the default
+ command line for preprocessing contains more options.
+ *)
+
+ val keep_comments: bool
+ (** [true] if the default preprocessor selected during compilation is
+ able to keep comments (hence ACSL annotations) in its output.
+ *)
+
+ val supported_arch_options: string list
+ (** architecture-related options (e.g. -m32) known to be supported by
+ the default preprocessor. Used to match preprocessor commands to
+ selected machdeps.
+ *)
+end
val is_gui: bool
(** Is the Frama-C GUI running?
@@ -48,68 +106,6 @@ val is_gui: bool
@since frama-c-trunk not anymore a reference
*)
-val datadirs: Filepath.Normalized.t list
-(** Directories where architecture independent files are in order of
- priority.
- @since 19.0-Potassium *)
-
-val datadir: Filepath.Normalized.t
-(** Last directory of datadirs (the directory of frama-c installation)
- @since 19.0-Potassium *)
-
-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 26.0-Iron *)
-
-val libdir: Filepath.Normalized.t
-(** Last directory of libdirs (the directory of frama-c installation)
- @since 26.0-Iron *)
-
-val plugin_dir: Filepath.Normalized.t list
-(** Directory where the Frama-C dynamic plug-ins are. *)
-
-val plugin_path: string
-(** The colon-separated concatenation of [plugin_dir].
- @since Magnesium-20151001 *)
-
-val preprocessor: string
-(** Name of the default command to call the preprocessor.
- If the CPP environment variable is set, use it
- else use the built-in default from autoconf. Usually this is
- "gcc -C -E -I."
- @since Oxygen-20120901 *)
-
-val using_default_cpp: bool
-(** whether the preprocessor command is the one defined at configure time
- or the result of taking a CPP environment variable, in case it differs
- from the configure-time command.
-
- @since Phosphorus-20170501-beta1 *)
-
-val preprocessor_is_gnu_like: bool
-(** whether the default preprocessor accepts the same options as gcc
- (i.e. is either gcc or clang), when this is the case, the default
- command line for preprocessing contains more options.
- @since Sodium-20150201
-*)
-
-val preprocessor_supported_arch_options: string list
-(** architecture-related options (e.g. -m32) known to be supported by
- the default preprocessor. Used to match preprocessor commands to
- selected machdeps.
- @since Phosphorus-20170501-beta1
-*)
-
-val preprocessor_keep_comments: bool
-(** [true] if the default preprocessor selected during compilation is
- able to keep comments (hence ACSL annotations) in its output.
- @since Neon-rc3
-*)
(*
Local Variables:
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 07ab04020e76e5fc46f4491607510ed03d21f5c2..6c2cd09b4ae3b7d7309a91cddaa17d97c76b9915 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -339,7 +339,7 @@ let process_stdlib_pragma name args =
match args with
| [ ACons ("pop",_) ] -> pop_stdheader (); None
| [ ACons ("push",_); AStr s ] ->
- let base_name = (System_config.framac_libc:>string) in
+ let base_name = (System_config.Share.libc:>string) in
let relative_name = Filepath.relativize ~base_name s in
push_stdheader relative_name;
None
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index cd1cb74879d9619c01ad59d891dcb68513579fb6..75717da4aa652a1ba697157aad0f2a819f28549b 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -388,7 +388,7 @@ let instantiate_available_templates type_table name (entry : builtin_template) =
let init_gcc_builtin_templates () =
let fp =
Datatype.Filepath.concat ~existence:Filepath.Must_exist
- System_config.datadir "compliance/gcc_builtins.json"
+ System_config.Share.main "compliance/gcc_builtins.json"
in
Json.init_builtin_templates ~default_compiler:GCC fp;
Gcc_builtin_templates_loaded.set true
@@ -396,7 +396,7 @@ let init_gcc_builtin_templates () =
let init_other_builtin_templates () =
let fp =
Datatype.Filepath.concat ~existence:Filepath.Must_exist
- System_config.datadir "compliance/compiler_builtins.json"
+ System_config.Share.main "compliance/compiler_builtins.json"
in
Json.init_builtin_templates fp
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index b70c0b9f5e9d12ef9ef7ab4255b13a7f7ac0ad67..9e5d005ddf2fe5ce5380c36a4a3657d3b3dd798e 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -81,9 +81,9 @@ let cpp_opt_kind () =
else Unknown
let is_cpp_gnu_like () =
- let open System_config in
+ let open System_config.Preprocessor in
let cpp_cmd = Kernel.CppCommand.get () in
- match cpp_cmd = "", using_default_cpp, preprocessor_is_gnu_like with
+ match cpp_cmd = "", is_default, is_gnu_like with
| true, true, true -> Gnu
| true, true, false -> Not_gnu
| _, _, _ -> cpp_opt_kind ()
@@ -92,10 +92,10 @@ let is_cpp_gnu_like () =
If the program has an explicit argument -cpp-command "XX -Y"
(quotes are required by the shell)
then XX -Y
- else use the command in [System_config.preprocessor].*)
+ else use the command in [System_config.Preprocessor.command].*)
let get_preprocessor_command () =
let cmdline = Kernel.CppCommand.get() in
- if cmdline <> "" then cmdline else System_config.preprocessor
+ if cmdline <> "" then cmdline else System_config.Preprocessor.command
let from_filename ?cpp f =
let cpp =
@@ -130,7 +130,7 @@ let from_filename ?cpp f =
if Hashtbl.mem check_suffixes suf then
External (f, suf)
else if cpp <> "" then begin
- if not System_config.preprocessor_keep_comments then
+ if not System_config.Preprocessor.keep_comments then
Kernel.warning ~once:true
"Default preprocessor does not keep comments. Any ACSL annotations \
on non-preprocessed files will be discarded.";
@@ -490,7 +490,7 @@ let build_cpp_cmd = function
let machdep_dir =
Machdep.generate_machdep_header ~censored_macros (get_machdep())
in
- [(machdep_dir:>string); (System_config.framac_libc:>string)]
+ [(machdep_dir:>string); (System_config.Share.libc:>string)]
end
else []
in
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 39bca3adf21e81280c93054357780ae3d6b349eb..3611c1f588e244c6ed8425cabf6db9acb4a775c3 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -114,7 +114,7 @@ let request_crash_report =
Note that a version and a backtrace alone often do not contain enough\n\
information to understand the bug. Guidelines for reporting bugs are at:\n\
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs\n"
- System_config.version_and_codename
+ System_config.Version.id_and_codename
let protect = function
| Sys.Break ->
@@ -1033,7 +1033,7 @@ let plugin_help shortname =
let help () =
Log.print_on_output
begin fun fmt ->
- Format.fprintf fmt "\nThis is Frama-C %s\n" System_config.version_and_codename ;
+ Format.fprintf fmt "\nThis is Frama-C %s\n" System_config.Version.id_and_codename ;
Format.fprintf fmt "\nUsage:\n %s [options files ...]\n" Sys.argv.(0) ;
let print_line fmt s =
Format.(pp_print_string fmt s ; pp_print_newline fmt ()) in
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 380a0e174cb95e0acd0a9651e17fefde8b6132f8..7d0e44b8cbdd324ad0058815a032afc5acae2a04 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -444,7 +444,7 @@ struct
(may be used if the plug-in is not installed at the same place as Frama-C)"
end)
(struct
- let dirs () = System_config.datadirs
+ let dirs () = System_config.Share.dirs
let visible_ref = !share_visible_ref
end)
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 37786e0941b60828c18ddfe925054efa978967b3..ec66fdebc1096de932680f2b40704a1d81132a43 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -448,7 +448,7 @@ let magic = 9 (* magic number *)
let save_projects selection projects filename =
let cout = open_out_bin (filename : Filepath.Normalized.t :> string) in
- output_value cout System_config.version;
+ output_value cout System_config.Version.id;
output_value cout magic;
output_value cout !Graph.Blocks.cpt_vertex;
let states : (t * (string * State.state_on_disk) list) list =
@@ -613,7 +613,7 @@ let load_projects ~project_under_copy selection ?name filename =
raise (IOError s)
end
in
- check_magic cin (fun x -> x) System_config.version;
+ check_magic cin (fun x -> x) System_config.Version.id;
check_magic cin (fun n -> "magic number " ^ string_of_int n) magic;
let ocamlgraph_counter = read cin in
let pre_existing_projects = Descr.init project_under_copy in
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index 316d2f22d153f6ee8f48b359c90825bebbfa3186..8cfee381861efc145d1e16ebd17f91d670211f49 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -151,7 +151,7 @@ let warn_builtin_override kf source bname =
let internal =
(* TODO: treat this 'internal' *)
let file = source.Filepath.pos_path in
- Filepath.is_relative ~base_name:System_config.datadir file
+ Filepath.is_relative ~base_name:System_config.Share.main file
in
if Kernel_function.is_definition kf && not internal
then
diff --git a/src/plugins/eva/utils/library_functions.ml b/src/plugins/eva/utils/library_functions.ml
index 1ab03581ef5aeb766ab846a065f7647ee37df260..e102542a0f6be3c1e8cdd0baa4d0878a91b01942 100644
--- a/src/plugins/eva/utils/library_functions.ml
+++ b/src/plugins/eva/utils/library_functions.ml
@@ -111,7 +111,7 @@ let warn_unsupported_spec name =
"@[The specification of function '%s' is currently not supported by Eva.@ \
Consider adding '%a'@ to the analyzed source files.@]"
name Filepath.Normalized.pretty
- (Filepath.Normalized.concat System_config.framac_libc header)
+ (Filepath.Normalized.concat System_config.Share.libc header)
with Not_found -> ()
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index a91fd7398bb7eef3d26e4ed5192f6a6c0cfaf389..33403999da9d1bd033efa5709bc5b7a94386b705 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1846,8 +1846,8 @@ class main_window () : main_window_extension_points =
end
let make_splash () =
- GMain.Rc.add_default_file ((System_config.datadir:>string) ^"/frama-c.rc");
- GMain.Rc.add_default_file ((System_config.datadir:>string) ^"/frama-c-user.rc");
+ GMain.Rc.add_default_file ((System_config.Share.main:>string) ^"/frama-c.rc");
+ GMain.Rc.add_default_file ((System_config.Share.main:>string) ^"/frama-c-user.rc");
(*print_endline ("BOOT: " ^ (Glib.Main.setlocale `ALL None));*)
let (_:string) = GtkMain.Main.init ~setlocale:false () in
(*print_endline ("START: " ^ (Glib.Main.setlocale `ALL None));*)
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 3971403b575b53f1191272ca1fef674e53f35814..4543cc17c76c8d9a35c51daadae8e100ce8c1a0e 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -294,7 +294,7 @@ module MYTREE = struct
let comes_from_share filename =
let path = Filepath.Normalized.of_string filename in
- Filepath.is_relative ~base_name:System_config.datadir path
+ Filepath.is_relative ~base_name:System_config.Share.main path
let is_function t = match t with
| MFile _ -> false
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 1dbb0fc1d5b6e7d6de04b5ad607fbdf12288eb2a..9879790fff9578c6b4aecf115d7ddc7262e7527a 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -24,7 +24,7 @@
let () =
begin
- Wutil.share := (System_config.datadir :> string);
+ Wutil.share := (System_config.Share.main :> string);
Wutil.flush := (fun msg -> Gui_parameters.warning "%s" msg);
end
@@ -32,7 +32,7 @@ let framac_logo, framac_icon =
try
let img ext =
Some (GdkPixbuf.from_file
- ((System_config.datadir:>string) ^ "/frama-c." ^ ext))
+ ((System_config.Share.main:>string) ^ "/frama-c." ^ ext))
in
img "png", img "ico"
with
diff --git a/src/plugins/gui/help_manager.ml b/src/plugins/gui/help_manager.ml
index a178673cdb3cc59524892369b6bc5cdbe59c39c0..d5e9ba63a562c8a370e8128cfb8ccb994b5ad2d9 100644
--- a/src/plugins/gui/help_manager.ml
+++ b/src/plugins/gui/help_manager.ml
@@ -100,7 +100,7 @@ let show main_ui =
~license
~website:"http://frama-c.com"
~website_label:"Questions and support"
- ~version:System_config.version_and_codename
+ ~version:System_config.Version.id_and_codename
~comments:"Frama-C is a suite of tools dedicated to the analysis of the \
source code of software written in C."
()
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 65e4d54cde82c5e8d63be8bb652a85db83df20ec..f450316a9de079c805eaf7c2fa62f95387f4fba6 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -28,7 +28,7 @@ let frama_c_sarif () =
if Mdr_params.SarifDeterministic.get () then
"0+omitted-for-deterministic-output", ""
else
- System_config.version_and_codename, System_config.version
+ System_config.Version.id_and_codename, System_config.Version.id
in
let fullName = name ^ "-" ^ version in
let downloadUri = "https://frama-c.com/download.html" in
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index 740bd0c5310960d306f1d09428a3a91949ac7a1d..3e3f2b501e1f3322a0485bb283313adcac6e13f3 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -107,10 +107,10 @@ let () =
~descr:(Md.plain "Frama-C Kernel configuration")
signature
begin fun rq () ->
- set_version rq System_config.version ;
- set_datadir rq (Filepath.Normalized.to_string_list System_config.datadirs);
+ set_version rq System_config.Version.id ;
+ set_datadir rq (Filepath.Normalized.to_string_list System_config.Share.dirs);
set_pluginpath rq
- (Filepath.Normalized.to_string_list System_config.plugin_dir) ;
+ (Filepath.Normalized.to_string_list System_config.Plugins.dirs) ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 8f8fd507bb3269ba1c9d911bd20831e66a28b00e..7c6fb95f3f71948133b2c7b68db389e3c62c5b7e 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -370,7 +370,7 @@ let dump ~root ?(meta=true) () =
Yojson.Basic.to_file (path:>string) maindata ;
let body =
[ Md.H1 (Md.plain "Presentation", None);
- Md.Block (Md.text (Md.format "Version %s" System_config.version))]
+ Md.Block (Md.text (Md.format "Version %s" System_config.Version.id))]
@
table_of_contents ()
@
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index aa94f15b3e009a0c8fd96382a24f848e28ee0eff..9c3a0f80149b2615ce73eae8987e742cefdcce2f 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -153,7 +153,7 @@ let get_name = function
| VCS.Why3 p -> Why3Provers.name p
let get_version = function
- | VCS.Qed | Tactical -> System_config.version_and_codename
+ | VCS.Qed | Tactical -> System_config.Version.id_and_codename
| Why3 p -> Why3Provers.version p
let iter_provers fn =
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index 3688f8074aeec40f43b0514a221cdb903c8f4fd0..c9ea93a9517933adeb43f9a0f816a9c0b3d2496a 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -130,7 +130,7 @@ let () =
let vis = new stdlib_visitor in
ignore (Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) (Ast.get ()));
let fc_stdlib_idents = vis#get_idents in
- let dir = Filename.concat (System_config.datadir:>string) "compliance" in
+ let dir = Filename.concat (System_config.Share.main:>string) "compliance" in
let c11_idents = Json.(to_table HeadersOnly (parse dir "c11_functions.json"))
and c11_headers = Json.(to_set (parse dir "c11_headers.json"))
and glibc_idents = Json.(to_set (parse dir "glibc_functions.json"))
diff --git a/tests/misc/version.ml b/tests/misc/version.ml
index 5c3fdae73bdd86978694b143ee6fa61879005e9d..cd75e4c34db5f49d5ca5137ef8bb5c60b95f7311 100644
--- a/tests/misc/version.ml
+++ b/tests/misc/version.ml
@@ -1,20 +1,20 @@
let re_version = Str.regexp "^\\([0-9]+\\)\\.\\([0-9]+\\)"
let run () =
- let version_str = System_config.version in
+ let version_str = System_config.Version.id in
if Str.string_match re_version version_str 0 then
let major = Str.matched_group 1 version_str in
let minor = Str.matched_group 2 version_str in
- if major = string_of_int System_config.major_version &&
- minor = string_of_int System_config.minor_version
+ if major = string_of_int System_config.Version.major &&
+ minor = string_of_int System_config.Version.minor
then
Kernel.feedback "version numbers match"
else
Kernel.abort
"error parsing major/minor version: expected %s.%s, got %d.%d"
- major minor System_config.major_version System_config.minor_version
+ major minor System_config.Version.major System_config.Version.minor
else
Kernel.abort
- "could not parse System_config.version"
+ "could not parse System_config.Version.id"
let () = Boot.Main.extend run