From aedae7e67ad6c89a7d1d4ef272e2d04eccec3c1d Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 5 Mar 2020 14:34:45 +0100
Subject: [PATCH] [config] change name of config.ml to avoid clash with
compiler internal lib
---
Makefile | 8 +-
Makefile.generating | 6 +-
bin/migration_scripts/calcium2scandium.sh | 178 ++++++++++++++++++
.../runtime/{config.ml.in => fc_config.ml.in} | 0
.../runtime/{config.mli => fc_config.mli} | 0
.../runtime/frama_c_config.ml.in | 12 +-
src/kernel_internals/runtime/gui_init.ml | 2 +-
src/kernel_internals/runtime/special_hooks.ml | 16 +-
.../runtime/toplevel_config.ml | 2 +-
src/kernel_internals/typing/cabs2cil.ml | 2 +-
src/kernel_services/ast_queries/file.ml | 18 +-
.../cmdline_parameters/cmdline.ml | 8 +-
.../plugin_entry_points/dynamic.ml | 16 +-
.../plugin_entry_points/kernel.ml | 1 -
.../plugin_entry_points/plugin.ml | 2 +-
src/libraries/project/project.ml | 4 +-
src/libraries/utils/command.ml | 2 +-
src/plugins/gui/design.ml | 4 +-
src/plugins/gui/filetree.ml | 2 +-
src/plugins/gui/gtk_helper.ml | 4 +-
src/plugins/gui/help_manager.ml | 2 +-
src/plugins/markdown-report/sarif_gen.ml | 4 +-
src/plugins/print_api/print_interface.ml | 2 +-
src/plugins/report/classify.ml | 2 +-
src/plugins/server/doc.ml | 8 +-
src/plugins/server/kernel_main.ml | 8 +-
src/plugins/value/domains/cvalue/builtins.ml | 2 +-
src/plugins/value/utils/library_functions.ml | 2 +-
src/plugins/wp/ProverWhy3.ml | 2 +-
src/plugins/wp/register.ml | 2 +-
src/plugins/wp/wp_parameters.ml | 4 +-
tests/libc/check_compliance.ml | 2 +-
tests/misc/version.ml | 10 +-
33 files changed, 256 insertions(+), 81 deletions(-)
create mode 100755 bin/migration_scripts/calcium2scandium.sh
rename src/kernel_internals/runtime/{config.ml.in => fc_config.ml.in} (100%)
rename src/kernel_internals/runtime/{config.mli => fc_config.mli} (100%)
diff --git a/Makefile b/Makefile
index d23384d9cc8..c680ae5bb8e 100644
--- a/Makefile
+++ b/Makefile
@@ -286,7 +286,7 @@ DISTRIB_FILES:=\
share/Makefile.dynamic_config.external \
share/Makefile.dynamic_config.internal \
share/META.frama-c \
- $(filter-out src/kernel_internals/runtime/config.ml, \
+ $(filter-out src/kernel_internals/runtime/fc_config.ml, \
$(wildcard src/kernel_internals/runtime/*.ml*)) \
$(wildcard src/kernel_services/abstract_interp/*.ml*) \
$(wildcard src/plugins/gui/*.ml*) \
@@ -474,7 +474,7 @@ CMO += $(LIB_CMO)
# Very first files to be linked (most modules use them)
###############################
-FIRST_CMO= src/kernel_internals/runtime/config \
+FIRST_CMO= src/kernel_internals/runtime/fc_config \
src/kernel_internals/runtime/gui_init \
src/kernel_services/plugin_entry_points/log \
src/kernel_services/cmdline_parameters/cmdline \
@@ -1324,8 +1324,8 @@ endif
#####################
CONFIG_DIR=src/kernel_internals/runtime
-CONFIG_FILE=$(CONFIG_DIR)/config.ml
-CONFIG_CMO=$(CONFIG_DIR)/config.cmo
+CONFIG_FILE=$(CONFIG_DIR)/fc_config.ml
+CONFIG_CMO=$(CONFIG_DIR)/fc_config.cmo
GENERATED +=$(CONFIG_FILE)
#Generated in Makefile.generating
diff --git a/Makefile.generating b/Makefile.generating
index a6bc1f96ad9..8d64ab4a1b4 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -176,13 +176,13 @@ src/libraries/stdlib/transitioning.ml: \
# Frama-C-config #
##################
-src/kernel_internals/runtime/frama_c_config.ml: src/kernel_internals/runtime/config.ml \
+src/kernel_internals/runtime/frama_c_config.ml: src/kernel_internals/runtime/fc_config.ml \
src/kernel_internals/runtime/frama_c_config.ml.in Makefile.generating
$(PRINT_MAKING) $@
$(RM) $@
$(ECHO) "module Filepath = struct let add_symbolic_dir _ _ = () end" >> $@
- $(ECHO) "module Config = struct" >> $@
- $(CAT) src/kernel_internals/runtime/config.ml >> $@
+ $(ECHO) "module Fc_config = struct" >> $@
+ $(CAT) src/kernel_internals/runtime/fc_config.ml >> $@
$(ECHO) "end" >> $@
$(CAT) src/kernel_internals/runtime/frama_c_config.ml.in >> $@
$(CHMOD_RO) $@
diff --git a/bin/migration_scripts/calcium2scandium.sh b/bin/migration_scripts/calcium2scandium.sh
new file mode 100755
index 00000000000..2369bb87b4f
--- /dev/null
+++ b/bin/migration_scripts/calcium2scandium.sh
@@ -0,0 +1,178 @@
+#! /bin/sh
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+#
+# Converts a Frama-C plugin from Frama-C 19 Potassium to Frama-C 20 Calcium,
+# on a best-efforts basis (no guarantee that the result is fully compatible).
+#
+# known missing features:
+# - doesn't work if a directory name contains spaces
+# - doesn't follow symbolic links to directories
+
+ARGS=$@
+
+DIR=
+
+# verbosing on by default
+VERBOSE="v"
+
+sedi ()
+{
+ if [ -n "`sed --help 2> /dev/null | grep \"\\-i\" 2> /dev/null`" ]; then
+ sed -i "$@"
+ else
+ # option '-i' is not recognized by sed: use a tmp file
+ new_temp=`mktemp /tmp/frama-c.XXXXXXX` || exit 1
+ sed "$@" > $new_temp
+ eval last=\${$#}
+ mv $new_temp $last
+ fi
+}
+
+dirs ()
+{
+ if [ -z "$DIR" ]; then
+ DIR=.
+ fi
+}
+
+safe_goto ()
+{
+ dir=$1
+ cd $dir
+ $3
+ cd $2
+}
+
+goto ()
+{
+ if [ -d $1 ]; then
+ safe_goto $1 $2 $3
+ else
+ echo "Directory '$1' does not exist. Omitted."
+ fi
+}
+
+process_file ()
+{
+ file=$1
+ if [ "$VERBOSE" ]; then
+ echo "Processing file $file"
+ fi
+ sedi \
+ -e 's/Config\.version/Fc_config.version/g' \
+ -e 's/Config\.codename/Fc_config.codename/g' \
+ -e 's/Config\.version_and_codename/Fc_config.version_and_codename/g' \
+ -e 's/Config\.major_version/Fc_config.major_version/g' \
+ -e 's/Config\.minor_version/Fc_config.minor_version/g' \
+ -e 's/Config\.is_gui/Fc_config.is_gui/g' \
+ -e 's/Config\.ocamlc/Fc_config.ocamlc/g' \
+ -e 's/Config\.ocamlopt/Fc_config.ocamlopt/g' \
+ -e 's/Config\.ocaml_wflags/Fc_config.ocaml_wflags/g' \
+ -e 's/Config\.datadir/Fc_config.datadir/g' \
+ -e 's/Config\.datadirs/Fc_config.datadirs/g' \
+ -e 's/Config\.framac_libc/Fc_config.framac_libc/g' \
+ -e 's/Config\.libdir/Fc_config.libdir/g' \
+ -e 's/Config\.plugin_dir/Fc_config.plugin_dir/g' \
+ -e 's/Config\.plugin_path/Fc_config.plugin_path/g' \
+ -e 's/Config\.compilation_unit_names/Fc_config.compilation_unit_names/g' \
+ -e 's/Config\.library_names/Fc_config.library_names/g' \
+ -e 's/Config\.preprocessor/Fc_config.preprocessor/g' \
+ -e 's/Config\.using_default_cpp/Fc_config.using_default_cpp/g' \
+ -e 's/Config\.preprocessor_is_gnu_like/Fc_config.preprocessor_is_gnu_like/g' \
+ -e 's/Config\.preprocessor_supported_arch_options/Fc_config.preprocessor_supported_arch_options/g' \
+ -e 's/Config\.preprocessor_keep_comments/Fc_config.preprocessor_keep_comments/g' \
+ -e 's/Config\.dot/Fc_config.dot/g' \
+ $file
+}
+
+apply_one_dir ()
+{
+ if [ "$VERBOSE" ]; then
+ echo "Processing directory `pwd`"
+ fi
+ for f in `ls -p1 *.ml* 2> /dev/null`; do
+ process_file $f
+ done
+}
+
+apply_recursively ()
+{
+ apply_one_dir
+ for d in `ls -p1 | grep \/`; do
+ safe_goto $d .. apply_recursively
+ done
+}
+
+applying_to_list ()
+{
+ dirs
+ tmpdir=`pwd`
+ for d in $DIR; do
+ goto $d $tmpdir $1
+ done
+}
+
+help ()
+{
+ echo "Usage: $0 [options | directories]
+
+Options are:
+ -r | --recursive Check subdirectories recursively
+ -h | --help Display help message
+ -q | --quiet Quiet mode (i.e. non-verbose mode)
+ -v | --verbose Verbose mode (default)"
+ exit 0
+}
+
+error ()
+{
+ echo "$1.
+Do \"$0 -h\" for help."
+ exit 1
+}
+
+FN="apply_one_dir"
+
+parse_arg ()
+{
+ case $1 in
+ -r | --recursive) FN="apply_recursively";;
+ -h | -help ) help; exit 0;;
+ -q | --quiet ) VERBOSE=;;
+ -v | --verbose ) VERBOSE="v";;
+ -* ) error "Invalid option $1";;
+ * ) DIR="$DIR $1";;
+ esac
+}
+
+cmd_line ()
+{
+ for s in $ARGS; do
+ parse_arg $s
+ done
+ applying_to_list $FN
+}
+
+cmd_line
+exit 0
diff --git a/src/kernel_internals/runtime/config.ml.in b/src/kernel_internals/runtime/fc_config.ml.in
similarity index 100%
rename from src/kernel_internals/runtime/config.ml.in
rename to src/kernel_internals/runtime/fc_config.ml.in
diff --git a/src/kernel_internals/runtime/config.mli b/src/kernel_internals/runtime/fc_config.mli
similarity index 100%
rename from src/kernel_internals/runtime/config.mli
rename to src/kernel_internals/runtime/fc_config.mli
diff --git a/src/kernel_internals/runtime/frama_c_config.ml.in b/src/kernel_internals/runtime/frama_c_config.ml.in
index 33e68c07b51..4b6d96b0879 100644
--- a/src/kernel_internals/runtime/frama_c_config.ml.in
+++ b/src/kernel_internals/runtime/frama_c_config.ml.in
@@ -32,26 +32,26 @@ let version _ =
FRAMAC_SHARE = %S@\n \
FRAMAC_LIB = %S@\n \
FRAMAC_PLUGIN = %S@."
- Config.version Config.codename
- Config.datadir Config.libdir Config.plugin_path
+ Fc_config.version Fc_config.codename
+ Fc_config.datadir Fc_config.libdir Fc_config.plugin_path
;
exit 0
let options = Arg.([
"-print-share-path",
- Unit (fun _ -> Format.printf "%s%!" Config.datadir; exit 0),
+ Unit (fun _ -> Format.printf "%s%!" Fc_config.datadir; exit 0),
" Print the path of Frama-C share directory";
"-print-libpath",
- Unit (fun _ -> Format.printf "%s%!" Config.libdir; exit 0),
+ Unit (fun _ -> Format.printf "%s%!" Fc_config.libdir; exit 0),
" Print the path of Frama-C kernel library";
"-print-plugin-path",
- Unit (fun _ -> Format.printf "%s%!" Config.plugin_path; exit 0),
+ Unit (fun _ -> Format.printf "%s%!" Fc_config.plugin_path; exit 0),
" Print the path where Frama-C dynamic plug-ins are searched for";
"-print-version",
- Unit (fun _ -> Format.printf "%s%!" Config.version; exit 0),
+ Unit (fun _ -> Format.printf "%s%!" Fc_config.version; exit 0),
" Print the version number of Frama-C";
"-version",
diff --git a/src/kernel_internals/runtime/gui_init.ml b/src/kernel_internals/runtime/gui_init.ml
index cbc7c365d7d..e01dc6f61c9 100644
--- a/src/kernel_internals/runtime/gui_init.ml
+++ b/src/kernel_internals/runtime/gui_init.ml
@@ -22,7 +22,7 @@
(** Frama-C GUI early initialization. *)
-let () = Config.is_gui := true
+let () = Fc_config.is_gui := true
let () = Unix.putenv "UBUNTU_MENUPROXY" "0"
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index bd62ca394f9..5b21630d6ba 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -38,12 +38,12 @@ let print_config () =
FRAMAC_SHARE = %S@\n \
FRAMAC_LIB = %S@\n \
FRAMAC_PLUGIN = %S%t@."
- Config.version_and_codename
- Config.datadir Config.libdir Config.plugin_path
+ Fc_config.version_and_codename
+ Fc_config.datadir Fc_config.libdir Fc_config.plugin_path
(fun fmt ->
- if Config.preprocessor = "" then
+ if Fc_config.preprocessor = "" then
Format.fprintf fmt "@\nWarning: no default pre-processor"
- else if not Config.preprocessor_keep_comments then
+ else if not Fc_config.preprocessor_keep_comments then
Format.fprintf fmt
"@\nWarning: default pre-processor is not able to keep comments \
(hence ACSL annotations) in its output")
@@ -59,17 +59,17 @@ let print_config get value () =
raise Cmdline.Exit
end
-let print_version = print_config Kernel.PrintVersion.get Config.version_and_codename
+let print_version = print_config Kernel.PrintVersion.get Fc_config.version_and_codename
let () = Cmdline.run_after_early_stage print_version
-let print_sharepath = print_config Kernel.PrintShare.get Config.datadir
+let print_sharepath = print_config Kernel.PrintShare.get Fc_config.datadir
let () = Cmdline.run_after_early_stage print_sharepath
-let print_libpath = print_config Kernel.PrintLib.get Config.libdir
+let print_libpath = print_config Kernel.PrintLib.get Fc_config.libdir
let () = Cmdline.run_after_early_stage print_libpath
let print_pluginpath =
- print_config Kernel.PrintPluginPath.get Config.plugin_path
+ print_config Kernel.PrintPluginPath.get Fc_config.plugin_path
let () = Cmdline.run_after_early_stage print_pluginpath
let print_machdep () =
diff --git a/src/kernel_internals/runtime/toplevel_config.ml b/src/kernel_internals/runtime/toplevel_config.ml
index bc028ff5700..0e6eba462cc 100644
--- a/src/kernel_internals/runtime/toplevel_config.ml
+++ b/src/kernel_internals/runtime/toplevel_config.ml
@@ -20,4 +20,4 @@
(* *)
(**************************************************************************)
-let () = Topdirs.dir_directory Config.libdir
+let () = Topdirs.dir_directory Fc_config.libdir
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 481fde16c7e..e8e0f215dfa 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -321,7 +321,7 @@ let process_stdlib_pragma name args =
match args with
| [ ACons ("pop",_) ] -> pop_stdheader (); None
| [ ACons ("push",_); AStr s ] ->
- let base_name = Config.framac_libc in
+ let base_name = Fc_config.framac_libc in
let relative_name = Filepath.relativize ~base_name s in
push_stdheader relative_name;
None
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index dff1e2a3fe3..99008be9f27 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -103,18 +103,18 @@ let cpp_opt_kind () =
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 [Config.preprocessor].*)
+ else use the command in [Fc_config.preprocessor].*)
let get_preprocessor_command () =
let cmdline = Kernel.CppCommand.get() in
if cmdline <> "" then begin
(cmdline, cpp_opt_kind ())
end else begin
let gnu =
- if Config.using_default_cpp then
- if Config.preprocessor_is_gnu_like then Gnu else Not_gnu
+ if Fc_config.using_default_cpp then
+ if Fc_config.preprocessor_is_gnu_like then Gnu else Not_gnu
else cpp_opt_kind ()
in
- Config.preprocessor, gnu
+ Fc_config.preprocessor, gnu
end
let from_filename ?cpp f =
@@ -144,7 +144,7 @@ let from_filename ?cpp f =
if Hashtbl.mem check_suffixes suf then
External (f, suf)
else if cpp <> "" then begin
- if not Config.preprocessor_keep_comments then
+ if not Fc_config.preprocessor_keep_comments then
Kernel.warning ~once:true
"Default pre-processor does not keep comments. Any ACSL annotation \
on non-pre-processed file will be discarded.";
@@ -460,7 +460,7 @@ let parse_cabs = function
(* Hypothesis: the preprocessor is POSIX compliant,
hence understands -I and -D. *)
let include_args =
- if Kernel.FramaCStdLib.get () then [Config.framac_libc]
+ if Kernel.FramaCStdLib.get () then [Fc_config.framac_libc]
else []
in
let define_args =
@@ -478,7 +478,7 @@ let parse_cabs = function
let required_cpp_arch_args = (get_machdep ()).cpp_arch_flags in
let supported_cpp_arch_args, unsupported_cpp_arch_args =
List.partition (fun arg ->
- List.mem arg Config.preprocessor_supported_arch_options)
+ List.mem arg Fc_config.preprocessor_supported_arch_options)
required_cpp_arch_args
in
if is_gnu_like = Unknown && not (Kernel.CppCommand.is_set ())
@@ -492,7 +492,7 @@ let parse_cabs = function
(Pretty_utils.pp_list ~sep:" " Format.pp_print_string)
unsupported_cpp_arch_args (Kernel.Machdep.get ())
(Pretty_utils.pp_list ~sep:" " Format.pp_print_string)
- Config.preprocessor_supported_arch_options;
+ Fc_config.preprocessor_supported_arch_options;
let extra_args =
if Kernel.ReadAnnot.get () then
if Kernel.PreprocessAnnot.is_set () then
@@ -1668,7 +1668,7 @@ let init_from_cmdline () =
Project.set_current prj2;
end;
let files = Kernel.Files.get () in
- if files = [] && not !Config.is_gui then Kernel.warning "no input file.";
+ if files = [] && not !Fc_config.is_gui then Kernel.warning "no input file.";
let files = List.map (fun f -> from_filename f) files in
try
init_from_c_files files;
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 1cb569973b7..5a166f93f07 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -71,7 +71,7 @@ module Kernel_log =
let dkey = Kernel_log.register_category "cmdline"
let quiet_ref = ref false
-let journal_enable_ref = ref !Config.is_gui
+let journal_enable_ref = ref !Fc_config.is_gui
let journal_isset_ref = ref false
let use_obj_ref = ref true
let use_type_ref = ref true
@@ -87,7 +87,7 @@ let long_plugin_name s =
if s = Log.kernel_label_name then "Frama-C" else "Plug-in " ^ s
let additional_info () =
- if !Config.is_gui then
+ if !Fc_config.is_gui then
"\nReverting to previous state.\n\
Check the Console tab for additional information."
else
@@ -111,7 +111,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\
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines\n"
- Config.version_and_codename
+ Fc_config.version_and_codename
let protect = function
| Sys.Break ->
@@ -993,7 +993,7 @@ let plugin_help shortname =
let help () =
Log.print_on_output
begin fun fmt ->
- Format.fprintf fmt "\nThis is Frama-C %s\n" Config.version_and_codename ;
+ Format.fprintf fmt "\nThis is Frama-C %s\n" Fc_config.version_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/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 1732542c4fd..5ff2f32c9fa 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -125,7 +125,7 @@ let is_object base =
let packages = Hashtbl.create 64
-let () = List.iter (fun p -> Hashtbl.add packages p ()) ("frama-c.kernel"::Config.library_names)
+let () = List.iter (fun p -> Hashtbl.add packages p ()) ("frama-c.kernel"::Fc_config.library_names)
let missing pkg = not (Hashtbl.mem packages pkg)
@@ -172,7 +172,7 @@ let load_packages pkgs =
- plugin(byte)
- plugin(native)
*)
- let gui = if !Config.is_gui then ["gui"] else [] in
+ let gui = if !Fc_config.is_gui then ["gui"] else [] in
let predicates =
(** The order is important for the archive cases *)
if Dynlink.is_native then
@@ -241,11 +241,11 @@ let load_script base =
let fmt = Format.formatter_of_buffer cmd in
begin
if Dynlink.is_native then
- Format.fprintf fmt "%s -shared -o %s.cmxs" Config.ocamlopt base
+ Format.fprintf fmt "%s -shared -o %s.cmxs" Fc_config.ocamlopt base
else
- Format.fprintf fmt "%s -c" Config.ocamlc ;
- Format.fprintf fmt " -g %s -warn-error a -I %s" Config.ocaml_wflags Config.libdir ;
- if !Config.is_gui then Format.pp_print_string fmt " -package lablgtk2" ;
+ Format.fprintf fmt "%s -c" Fc_config.ocamlc ;
+ Format.fprintf fmt " -g %s -warn-error a -I %s" Fc_config.ocaml_wflags Fc_config.libdir ;
+ if !Fc_config.is_gui then Format.pp_print_string fmt " -package lablgtk2" ;
List.iter (fun p -> Format.fprintf fmt " -I %s" p) !load_path ;
Format.fprintf fmt " %s.ml" base ;
Format.pp_print_flush fmt () ;
@@ -283,10 +283,10 @@ let set_module_load_path path =
( if user then Klog.warning "cannot load '%s' (not a directory)" d
; ps ) in
Klog.debug ~dkey "plugin_dir: %s"
- (String.concat ocamlfind_path_separator Config.plugin_dir);
+ (String.concat ocamlfind_path_separator Fc_config.plugin_dir);
load_path :=
List.fold_right (add_dir ~user:true) path
- (List.fold_right (add_dir ~user:false) (Config.libdir::Config.plugin_dir) []);
+ (List.fold_right (add_dir ~user:false) (Fc_config.libdir::Fc_config.plugin_dir) []);
let env_ocamlpath =
try Str.split (Str.regexp ocamlfind_path_separator) (Sys.getenv "OCAMLPATH")
with Not_found -> []
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 23bf7d9f478..cce382d5d4e 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -25,7 +25,6 @@
(* ************************************************************************* *)
module CamlString = String
-module Fc_config = Config
let () = Plugin.register_kernel ()
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 65121c53f78..667d8aeef6e 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -394,7 +394,7 @@ struct
(may be used if the plug-in is not installed at the same place as Frama-C)"
end)
(struct
- let dirs () = Config.datadirs
+ let dirs () = Fc_config.datadirs
let visible_ref = !share_visible_ref
let force_dir = false
end)
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 41cbba0b33f..0c436d88610 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -521,7 +521,7 @@ let magic = 9 (* magic number *)
let save_projects selection projects filename =
if Cmdline.use_obj then begin
let cout = open_out_bin filename in
- output_value cout Config.version;
+ output_value cout Fc_config.version;
output_value cout magic;
output_value cout !Graph.Blocks.cpt_vertex;
let states : (t * (string * State.state_on_disk) list) list =
@@ -708,7 +708,7 @@ let load_projects ~project_under_copy selection ?name filename =
raise (IOError s)
end
in
- check_magic cin (fun x -> x) Config.version;
+ check_magic cin (fun x -> x) Fc_config.version;
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/libraries/utils/command.ml b/src/libraries/utils/command.ml
index 45b31c884d8..be4593d70d7 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -238,7 +238,7 @@ let command_async ?stdout ?stderr cmd args =
command_generic ~async:true ?stdout ?stderr cmd args
let command ?(timeout=0) ?stdout ?stderr cmd args =
- if !Config.is_gui || timeout > 0 then
+ if !Fc_config.is_gui || timeout > 0 then
let f = command_generic ~async:true ?stdout ?stderr cmd args in
let res = ref(Unix.WEXITED 99) in
let ftimeout = float_of_int timeout in
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 8c8c16416f6..dee262fbb10 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1806,8 +1806,8 @@ class main_window () : main_window_extension_points =
end
let make_splash () =
- GMain.Rc.add_default_file (Config.datadir ^"/frama-c.rc");
- GMain.Rc.add_default_file (Config.datadir ^"/frama-c-user.rc");
+ GMain.Rc.add_default_file (Fc_config.datadir ^"/frama-c.rc");
+ GMain.Rc.add_default_file (Fc_config.datadir ^"/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 22d070fd84b..69b3c42024f 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -294,7 +294,7 @@ module MYTREE = struct
Cil.hasAttribute "FC_BUILTIN" (Cil_datatype.Global.attr g)
let comes_from_share filename =
- Filepath.is_relative ~base_name:Config.datadir filename
+ Filepath.is_relative ~base_name:Fc_config.datadir filename
let is_stdlib_global g =
Cil.hasAttribute "fc_stdlib" (Cil_datatype.Global.attr g) ||
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 48b2b6d40bd..298d75d184f 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -24,14 +24,14 @@
let () =
begin
- Wutil.share := Config.datadir;
+ Wutil.share := Fc_config.datadir;
Wutil.flush := (fun msg -> Gui_parameters.warning "%s" msg);
end
let framac_logo, framac_icon =
try
let img ext =
- Some (GdkPixbuf.from_file (Config.datadir ^ "/frama-c." ^ ext))
+ Some (GdkPixbuf.from_file (Fc_config.datadir ^ "/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 0156c2030ff..68983f58f9e 100644
--- a/src/plugins/gui/help_manager.ml
+++ b/src/plugins/gui/help_manager.ml
@@ -89,7 +89,7 @@ let show main_ui =
~license
~website:"http://frama-c.com"
~website_label:"Questions and support"
- ~version:Config.version_and_codename
+ ~version:Fc_config.version_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 dd043d7b74e..f3e3ed9226d 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -24,8 +24,8 @@ open Sarif
let frama_c_sarif =
let name = "frama-c" in
- let version = Config.version_and_codename in
- let semanticVersion = Config.version in
+ let version = Fc_config.version_and_codename in
+ let semanticVersion = Fc_config.version in
let fullName = name ^ "-" ^ version in
let downloadUri = "https://frama-c.com/download.html" in
Tool.create
diff --git a/src/plugins/print_api/print_interface.ml b/src/plugins/print_api/print_interface.ml
index c1492a8c3ba..539a3f63767 100644
--- a/src/plugins/print_api/print_interface.ml
+++ b/src/plugins/print_api/print_interface.ml
@@ -58,7 +58,7 @@ let type_to_add: (string, string * string) Hashtbl.t = Hashtbl.create 97
let clash_with_compilation_unit =
let h = Hashtbl.create 97 in
- List.iter (fun s -> Hashtbl.add h s ()) Config.compilation_unit_names;
+ List.iter (fun s -> Hashtbl.add h s ()) Fc_config.compilation_unit_names;
fun s ->
Hashtbl.mem h s || Hashtbl.mem h (String.lowercase_ascii s)
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 82fb8d6d0fc..ba15f820bfa 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -547,7 +547,7 @@ let classify () =
report_number "Unclassified: " !nb_unclassified R.OutputUnclassified.get ;
if !nb_errors > 0 && R.Exit.get () then
R.abort "Classified errors found" ;
- if not !Config.is_gui then clear_events () ;
+ if not !Fc_config.is_gui then clear_events () ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/doc.ml b/src/plugins/server/doc.ml
index d91eedd7885..cab11780aec 100644
--- a/src/plugins/server/doc.ml
+++ b/src/plugins/server/doc.ml
@@ -66,12 +66,12 @@ let page chapter ~title ~filename =
with Not_found ->
let intro = match chapter with
| `Protocol ->
- Printf.sprintf "%s/server/protocol/%s" Config.datadir filename
+ Printf.sprintf "%s/server/protocol/%s" Fc_config.datadir filename
| `Kernel ->
- Printf.sprintf "%s/server/kernel/%s" Config.datadir filename
+ Printf.sprintf "%s/server/kernel/%s" Fc_config.datadir filename
| `Plugin name ->
if not (List.mem name !plugins) then plugins := name :: !plugins ;
- Printf.sprintf "%s/%s/server/%s" Config.datadir name filename in
+ Printf.sprintf "%s/%s/server/%s" Fc_config.datadir name filename in
let intro =
if Sys.file_exists intro
then Markdown.rawfile intro
@@ -221,7 +221,7 @@ let dump ~root ?(meta=true) () =
Yojson.Basic.to_file path maindata ;
let body =
[ H1 (plain "Documentation", None);
- Block (text (format "Version %s" Config.version))]
+ Block (text (format "Version %s" Fc_config.version))]
@
table_of_contents ()
@
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index fefac224236..22866e37d79 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -50,10 +50,10 @@ let () =
(module Jstring.Jlist) in
Request.register_sig get_config
begin fun rq () ->
- set_version rq Config.version ;
- set_datadir rq Config.datadir ;
- set_libdir rq Config.libdir ;
- set_pluginpath rq Config.plugin_dir ;
+ set_version rq Fc_config.version ;
+ set_datadir rq Fc_config.datadir ;
+ set_libdir rq Fc_config.libdir ;
+ set_pluginpath rq Fc_config.plugin_dir ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 688f33b7f98..2558f8efefb 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -140,7 +140,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:Config.datadir (file :> string)
+ Filepath.is_relative ~base_name:Fc_config.datadir (file :> string)
in
if Kernel_function.is_definition kf && not internal
then
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index 4948f0892de..e3c5407e4b4 100644
--- a/src/plugins/value/utils/library_functions.ml
+++ b/src/plugins/value/utils/library_functions.ml
@@ -99,7 +99,7 @@ let warn_unsupported_spec name =
~wkey:Value_parameters.wkey_libc_unsupported_spec
"@[The specification of function '%s' is currently not supported by Eva.@ \
Consider adding %s@ to the analyzed source files.@]"
- name (Config.datadir ^ "/libc/" ^ header)
+ name (Fc_config.datadir ^ "/libc/" ^ header)
with Not_found -> ()
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index ef58b57e3e7..f8d633e00f2 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1185,7 +1185,7 @@ let get_miss () = !miss
let get_removed () = !removed
let mark_cache ~mode hash =
- if mode = Cleanup || !Config.is_gui then Hashtbl.replace cleanup hash ()
+ if mode = Cleanup || !Fc_config.is_gui then Hashtbl.replace cleanup hash ()
let cleanup_cache ~mode =
if mode = Cleanup && (!hits > 0 || !miss > 0) then
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index b99a36febdc..509dbcb3e7b 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -945,7 +945,7 @@ let () = Cmdline.run_after_setting_files
let () = Cmdline.run_after_configuring_stage Why3Provers.configure
let do_prover_detect () =
- if not !Config.is_gui && Wp_parameters.Detect.get () then
+ if not !Fc_config.is_gui && Wp_parameters.Detect.get () then
let provers = Why3Provers.provers () in
if provers = [] then
Wp_parameters.result "No Why3 provers detected."
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 8202d68da17..219694d2e8f 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -20,8 +20,6 @@
(* *)
(**************************************************************************)
-module Fc_Config = Config
-
let () = Plugin.is_share_visible ()
let () = Plugin.is_session_visible ()
include Plugin.Register
@@ -1078,7 +1076,7 @@ let base_output () =
| None -> let output =
match OutputDir.get () with
| "" ->
- if !Fc_Config.is_gui
+ if !Fc_config.is_gui
then make_gui_dir ()
else make_tmp_dir ()
| dir ->
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index ce69f25c601..6fa7f52646e 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -92,7 +92,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 Config.datadir "compliance" in
+ let dir = Filename.concat Fc_config.datadir "compliance" in
let c11_idents = get_ident_headers dir "c11_functions.json" in
let glibc_idents = get_idents dir "glibc_functions.json" in
let posix_idents = get_ident_headers_and_extensions dir "posix_identifiers.json" in
diff --git a/tests/misc/version.ml b/tests/misc/version.ml
index 2105830a936..c51486acaec 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 = Config.version in
+ let version_str = Fc_config.version 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 Config.major_version &&
- minor = string_of_int Config.minor_version
+ if major = string_of_int Fc_config.major_version &&
+ minor = string_of_int Fc_config.minor_version
then
Kernel.feedback "version numbers match"
else
Kernel.abort
"error parsing major/minor version: expected %s.%s, got %d.%d"
- major minor Config.major_version Config.minor_version
+ major minor Fc_config.major_version Fc_config.minor_version
else
Kernel.abort
- "could not parse Config.version"
+ "could not parse Fc_config.version"
let () = Db.Main.extend run
--
GitLab