diff --git a/.Makefile.lint b/.Makefile.lint
index b48bf3c53ff5260e2504cf1acfe877b4b0c18654..45b0947948bf34583b88506bce3b0b8c9fc134d0 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -5,7 +5,6 @@ ML_LINT_KO+=src/kernel_internals/parsing/errorloc.mli
ML_LINT_KO+=src/kernel_internals/parsing/lexerhack.ml
ML_LINT_KO+=src/kernel_internals/parsing/logic_preprocess.mli
ML_LINT_KO+=src/kernel_internals/runtime/boot.ml
-ML_LINT_KO+=src/kernel_internals/runtime/config.mli
ML_LINT_KO+=src/kernel_internals/runtime/machdeps.ml
ML_LINT_KO+=src/kernel_internals/runtime/messages.ml
ML_LINT_KO+=src/kernel_internals/runtime/messages.mli
diff --git a/.gitignore b/.gitignore
index 2b8b272dc8c3db14beee19536f597b09aac0f460..b4fbb18004f8bab9db8d701d49adff8526b9d748 100644
--- a/.gitignore
+++ b/.gitignore
@@ -39,6 +39,7 @@ autom4te.cache
/ocamlgraph/
*.check_mli_exists
.Makefile.plugin.generated
+.ocamldebug
#tests
@@ -185,7 +186,7 @@ Makefile.plugin.generated
/src/libraries/utils/json.ml
/src/kernel_internals/runtime/toplevel_boot.ml
-/src/kernel_internals/runtime/config.ml
+/src/kernel_internals/runtime/fc_config.ml
/src/kernel_internals/runtime/frama_c_config.ml
/src/kernel_internals/parsing/logic_lexer.ml
/src/kernel_internals/parsing/logic_parser.ml
diff --git a/Makefile b/Makefile
index d23384d9cc82b840853975b0b8f3abd9b5acc664..c680ae5bb8e22d84b1ae085f673d7963a95a32ac 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 a6bc1f96ad9432c135b93a073a4c8dcd832ab41c..e1793bede2262382953381b03a1e62734623a165 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -133,6 +133,7 @@ ifeq ($(HAS_OCAML408),yes)
Format.String_tag str -> str \
| _ -> raise (Invalid_argument "unsupported tag extension")
FORMAT_STAG_OF_STRING=Format.String_tag s
+ FORMAT_PP_OPT=Format.pp_print_option
HAS_OCAML407_OR_408=yes
else
DYNLINK_INIT=Dynlink.init
@@ -144,6 +145,10 @@ else
else
HAS_OCAML407_OR_408=no
endif
+ FORMAT_PP_OPT=fun ?(none=(fun _ () -> ())) pp fmt o -> \
+ match o with \
+ | None -> none fmt () \
+ | Some v -> pp fmt v
endif
ifeq ($(HAS_OCAML407_OR_408),yes)
@@ -169,6 +174,7 @@ src/libraries/stdlib/transitioning.ml: \
-e 's/@FORMAT_STAG@/$(FORMAT_STAG)/g' \
-e 's/@FORMAT_STRING_OF_STAG@/$(FORMAT_STRING_OF_STAG)/g' \
-e 's/@FORMAT_STAG_OF_STRING@/$(FORMAT_STAG_OF_STRING)/g' \
+ -e 's/@FORMAT_PP_OPT@/$(FORMAT_PP_OPT)/g' \
$< > $@
$(CHMOD_RO) $@
@@ -176,13 +182,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/frama-c.debug b/bin/frama-c.debug
new file mode 100755
index 0000000000000000000000000000000000000000..89d9b58a60320637d298fbc80b9714ea19afb702
--- /dev/null
+++ b/bin/frama-c.debug
@@ -0,0 +1,172 @@
+#!/bin/sh
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# 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). #
+# #
+##########################################################################
+
+
+. $(dirname $0)/local_export.sh
+
+if test ! -e .ocamldebug; then
+ GEN_OCAMLDEBUG=yes;
+ cat <<EOF > .ocamldebug;
+load_printer "str.cma"
+load_printer "zarith.cma"
+load_printer "dynlink.cma"
+load_printer "extlib.cmo"
+load_printer "filepath.cmo"
+load_printer "integer.cmo"
+load_printer "transitioning.cmo"
+load_printer "pretty_utils.cmo"
+load_printer "cil_types_debug.cmo"
+load_printer "cabs_debug.cmo"
+
+install_printer Cil_types_debug.pp_integer
+install_printer Cil_types_debug.pp_variant
+install_printer Cil_types_debug.pp_allocation
+install_printer Cil_types_debug.pp_deps
+install_printer Cil_types_debug.pp_from
+install_printer Cil_types_debug.pp_assigns
+install_printer Cil_types_debug.pp_file
+install_printer Cil_types_debug.pp_global
+install_printer Cil_types_debug.pp_typ
+install_printer Cil_types_debug.pp_ikind
+install_printer Cil_types_debug.pp_fkind
+install_printer Cil_types_debug.pp_bitsSizeofTyp
+install_printer Cil_types_debug.pp_bitsSizeofTypCache
+install_printer Cil_types_debug.pp_attribute
+install_printer Cil_types_debug.pp_attributes
+install_printer Cil_types_debug.pp_attrparam
+install_printer Cil_types_debug.pp_compinfo
+install_printer Cil_types_debug.pp_fieldinfo
+install_printer Cil_types_debug.pp_enuminfo
+install_printer Cil_types_debug.pp_enumitem
+install_printer Cil_types_debug.pp_typeinfo
+install_printer Cil_types_debug.pp_varinfo
+install_printer Cil_types_debug.pp_storage
+install_printer Cil_types_debug.pp_exp
+install_printer Cil_types_debug.pp_exp_node
+install_printer Cil_types_debug.pp_exp_info
+install_printer Cil_types_debug.pp_constant
+install_printer Cil_types_debug.pp_unop
+install_printer Cil_types_debug.pp_binop
+install_printer Cil_types_debug.pp_lval
+install_printer Cil_types_debug.pp_lhost
+install_printer Cil_types_debug.pp_offset
+install_printer Cil_types_debug.pp_init
+install_printer Cil_types_debug.pp_initinfo
+install_printer Cil_types_debug.pp_fundec
+install_printer Cil_types_debug.pp_block
+install_printer Cil_types_debug.pp_stmt
+install_printer Cil_types_debug.pp_label
+install_printer Cil_types_debug.pp_stmtkind
+install_printer Cil_types_debug.pp_catch_binder
+install_printer Cil_types_debug.pp_instr
+install_printer Cil_types_debug.pp_extended_asm
+install_printer Cil_types_debug.pp_filepath_position
+install_printer Cil_types_debug.pp_lexing_position
+install_printer Cil_types_debug.pp_location
+install_printer Cil_types_debug.pp_logic_constant
+install_printer Cil_types_debug.pp_logic_real
+install_printer Cil_types_debug.pp_logic_type
+install_printer Cil_types_debug.pp_identified_term
+install_printer Cil_types_debug.pp_logic_label
+install_printer Cil_types_debug.pp_logic_builtin_label
+install_printer Cil_types_debug.pp_term
+install_printer Cil_types_debug.pp_term_node
+install_printer Cil_types_debug.pp_term_lval
+install_printer Cil_types_debug.pp_term_lhost
+install_printer Cil_types_debug.pp_model_info
+install_printer Cil_types_debug.pp_term_offset
+install_printer Cil_types_debug.pp_logic_info
+install_printer Cil_types_debug.pp_builtin_logic_info
+install_printer Cil_types_debug.pp_logic_body
+install_printer Cil_types_debug.pp_logic_type_info
+install_printer Cil_types_debug.pp_logic_type_def
+install_printer Cil_types_debug.pp_logic_var_kind
+install_printer Cil_types_debug.pp_logic_var
+install_printer Cil_types_debug.pp_logic_ctor_info
+install_printer Cil_types_debug.pp_quantifiers
+install_printer Cil_types_debug.pp_relation
+install_printer Cil_types_debug.pp_predicate_node
+install_printer Cil_types_debug.pp_identified_predicate
+install_printer Cil_types_debug.pp_predicate
+install_printer Cil_types_debug.pp_spec
+install_printer Cil_types_debug.pp_acsl_extension
+install_printer Cil_types_debug.pp_acsl_extension_kind
+install_printer Cil_types_debug.pp_loop_pragma
+install_printer Cil_types_debug.pp_slice_pragma
+install_printer Cil_types_debug.pp_impact_pragma
+install_printer Cil_types_debug.pp_pragma
+install_printer Cil_types_debug.pp_code_annotation_node
+install_printer Cil_types_debug.pp_funspec
+install_printer Cil_types_debug.pp_code_annotation
+install_printer Cil_types_debug.pp_funbehavior
+install_printer Cil_types_debug.pp_global_annotation
+install_printer Cil_types_debug.pp_custom_tree
+install_printer Cil_types_debug.pp_kinstr
+install_printer Cil_types_debug.pp_cil_function
+install_printer Cil_types_debug.pp_kernel_function
+install_printer Cil_types_debug.pp_localisation
+install_printer Cil_types_debug.pp_mach
+
+install_printer Cabs_debug.pp_cabsloc
+install_printer Cabs_debug.pp_storage
+install_printer Cabs_debug.pp_fun_spec
+install_printer Cabs_debug.pp_cvspec
+install_printer Cabs_debug.pp_const
+install_printer Cabs_debug.pp_labels
+install_printer Cabs_debug.pp_typeSpecifier
+install_printer Cabs_debug.pp_spec_elem
+install_printer Cabs_debug.pp_spec
+install_printer Cabs_debug.pp_decl_type
+install_printer Cabs_debug.pp_name_group
+install_printer Cabs_debug.pp_field_group
+install_printer Cabs_debug.pp_field_groups
+install_printer Cabs_debug.pp_init_name_group
+install_printer Cabs_debug.pp_name
+install_printer Cabs_debug.pp_init_name
+install_printer Cabs_debug.pp_single_name
+install_printer Cabs_debug.pp_enum_item
+install_printer Cabs_debug.pp_def
+install_printer Cabs_debug.pp_block
+install_printer Cabs_debug.pp_raw_stmt
+install_printer Cabs_debug.pp_stmt
+install_printer Cabs_debug.pp_for_clause
+install_printer Cabs_debug.pp_bin_op
+install_printer Cabs_debug.pp_un_op
+install_printer Cabs_debug.pp_exp
+install_printer Cabs_debug.pp_exp_node
+install_printer Cabs_debug.pp_init_exp
+install_printer Cabs_debug.pp_initwhat
+install_printer Cabs_debug.pp_attr
+install_printer Cabs_debug.pp_attrs
+install_printer Cabs_debug.pp_file
+EOF
+else
+GEN_OCAMLDEBUG=no;
+fi
+
+ocamldebug -I $(ocamlfind query zarith) -I $(ocamlfind query ocamlgraph) \
+ -I $FRAMAC_LIB $BINDIR/toplevel.byte "$@"
+
+if test "$GEN_OCAMLDEBUG" = "yes"; then
+ rm .ocamldebug;
+fi
diff --git a/bin/migration_scripts/calcium2scandium.sh b/bin/migration_scripts/calcium2scandium.sh
new file mode 100755
index 0000000000000000000000000000000000000000..f1c05c3634d837f37b8267efd9e9df07a08c3d8f
--- /dev/null
+++ b/bin/migration_scripts/calcium2scandium.sh
@@ -0,0 +1,178 @@
+#! /bin/sh
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# 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/headers/headache_config.txt b/headers/headache_config.txt
index 17a5e0df7c761c8b616ded712cf0a62bca2d9de8..969d2cf13811e6a07cc2f3079c95c78d3e711606 100644
--- a/headers/headache_config.txt
+++ b/headers/headache_config.txt
@@ -53,6 +53,8 @@
| ".*frama-c.byte" -> skip match:"#!.*"
| "frama-c.top" -> frame open:"#" line:"#" close:"#"
| ".*frama-c.top" -> skip match:"#!.*"
+| "frama-c.debug" -> frame open:"#" line:"#" close:"#"
+| ".*frama-c.debug" -> skip match:"#!.*"
################
# Perl scripts #
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 88e6eb60c47818a2562f0e01ebde0465cbc4a49c..1af383628305ad5473354fdc8a5e75efb7f53714 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -22,10 +22,12 @@ bin/frama-c-script: CEA_LGPL
bin/frama-c-gui: CEA_LGPL
bin/frama-c-gui.byte: CEA_LGPL
bin/frama-c.byte: CEA_LGPL
+bin/frama-c.debug: CEA_LGPL
bin/frama-c.top: CEA_LGPL
bin/local_export.sh: CEA_LGPL
bin/migration_scripts/aluminium2silicon.sh: CEA_LGPL
bin/migration_scripts/boron2carbon.sh: CEA_LGPL
+bin/migration_scripts/calcium2scandium.sh: CEA_LGPL
bin/migration_scripts/carbon2nitrogen.sh: CEA_LGPL
bin/migration_scripts/fluorine2neon.sh: CEA_LGPL
bin/migration_scripts/lithium2beryllium.sh: CEA_LGPL
@@ -364,8 +366,8 @@ src/kernel_internals/parsing/logic_preprocess.mli: CEA_INRIA_LGPL
src/kernel_internals/parsing/logic_preprocess.mll: CEA_INRIA_LGPL
src/kernel_internals/runtime/README.md: .ignore
src/kernel_internals/runtime/boot.ml: CEA_LGPL
-src/kernel_internals/runtime/config.ml.in: CEA_LGPL
-src/kernel_internals/runtime/config.mli: CEA_LGPL
+src/kernel_internals/runtime/fc_config.ml.in: CEA_LGPL
+src/kernel_internals/runtime/fc_config.mli: CEA_LGPL
src/kernel_internals/runtime/frama_c_config.ml.in: CEA_LGPL
src/kernel_internals/runtime/frama_c_init.ml: CEA_LGPL
src/kernel_internals/runtime/frama_c_init.mli: CEA_LGPL
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 56%
rename from src/kernel_internals/runtime/config.mli
rename to src/kernel_internals/runtime/fc_config.mli
index 774ed39765c8c945805b1428d252d2c8acc49827..1b9c799d3a4533995bd43d597a76d9e8c65b6067 100644
--- a/src/kernel_internals/runtime/config.mli
+++ b/src/kernel_internals/runtime/fc_config.mli
@@ -43,88 +43,88 @@ val minor_version: int
@since 19.0-Potassium *)
val is_gui: bool ref
- (** Is the Frama-C GUI running?
- @since Beryllium-20090601-beta1 *)
+(** Is the Frama-C GUI running?
+ @since Beryllium-20090601-beta1 *)
val ocamlc: string
- (** Name of the bytecode compiler.
- @since Boron-20100401 *)
+(** Name of the bytecode compiler.
+ @since Boron-20100401 *)
val ocamlopt: string
- (** Name of the native compiler.
- @since Boron-20100401 *)
+(** Name of the native compiler.
+ @since Boron-20100401 *)
val ocaml_wflags: string
- (** Warning flags used when compiling Frama-C.
- @since Chlorine-20180501 *)
+(** Warning flags used when compiling Frama-C.
+ @since Chlorine-20180501 *)
val datadir: string
- (** Directory where architecture independent files are.
- Main directory, use {!datadirs} for the others *)
+(** Directory where architecture independent files are.
+ Main directory, use {!datadirs} for the others *)
val datadirs: string list
- (** Directories where architecture independent files are in order of
- priority.
- @since 19.0-Potassium *)
+(** Directories where architecture independent files are in order of
+ priority.
+ @since 19.0-Potassium *)
val framac_libc: string
- (** Directory where Frama-C libc headers are.
- @since 19.0-Potassium *)
+(** Directory where Frama-C libc headers are.
+ @since 19.0-Potassium *)
val libdir: string
- (** Directory where the Frama-C kernel library is.
- @since Beryllium-20090601-beta1 *)
+(** Directory where the Frama-C kernel library is.
+ @since Beryllium-20090601-beta1 *)
val plugin_dir: string list
- (** Directory where the Frama-C dynamic plug-ins are.
- @modify Magnesium-20151001 *)
+(** Directory where the Frama-C dynamic plug-ins are.
+ @modify Magnesium-20151001 *)
val plugin_path: string
- (** The coma-separated concatenation of [plugin_dir].
- @since Magnesium-20151001 *)
+(** The coma-separated concatenation of [plugin_dir].
+ @since Magnesium-20151001 *)
val compilation_unit_names: string list
- (** List of names of all kernel compilation units.
- @since Boron-20100401 *)
+(** List of names of all kernel compilation units.
+ @since Boron-20100401 *)
val library_names: string list
- (** List of linked libraries.
- @since Magnesium-20151001 *)
+(** List of linked libraries.
+ @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 *)
+(** 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.
+(** 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 *)
+ @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 pre-processing contains more options.
- @since Sodium-20150201
- *)
+(** 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 pre-processing 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
- *)
+(** 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
- *)
-
+(** [true] if the default preprocessor selected during compilation is
+ able to keep comments (hence ACSL annotations) in its output.
+ @since Neon-rc3
+*)
+
val dot: string option
(** Dot command name.
@return [None] if `dot' is not installed.
diff --git a/src/kernel_internals/runtime/frama_c_config.ml.in b/src/kernel_internals/runtime/frama_c_config.ml.in
index 33e68c07b519cf1d28e6b32a86cc5127d00866c9..4b6d96b08791de028a4b730c2c13c8064834fbfd 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 cbc7c365d7d4df2a0c7b8e967cc33f2772ef37ac..e01dc6f61c92e28d9a758dd4b1502f7258a5cd9b 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 bd62ca394f9df1e1dcc7f721ef0bb7dcc967f958..5b21630d6ba2b12acb71c8225808b1d16d058161 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 bc028ff57001fcdb209b6eb227f301cf7e3b06e0..0e6eba462cc4dcad44241f970c6cad726dd7b431 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 481fde16c7eb3a4bf955c7730e5107c74cd29c0c..e8e0f215dfae702cabb820957ec3f6f1402ec119 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_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index 3903899e1fe7b0849642f16e48a5fbfdbbb60c14..f7ea40bd18f2c9b3c9e3acf4a2369ae078021e2e 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -250,17 +250,17 @@ and pp_raw_stmt fmt = function
pp_block bl1 pp_block bl2 pp_cabsloc loc
| THROW(e,loc) ->
fprintf fmt "@[<hov 2>THROW %a, loc(%a)@]"
- (Pretty_utils.pp_opt pp_exp) e pp_cabsloc loc
+ (Transitioning.Format.pp_print_option pp_exp) e pp_cabsloc loc
| TRY_CATCH(s,l,loc) ->
let print_one_catch fmt (v,s) =
fprintf fmt "@[<v 2>@[CATCH %a {@]@;%a@]@;}"
- (Pretty_utils.pp_opt pp_single_name) v
+ (Transitioning.Format.pp_print_option pp_single_name) v
pp_stmt s
in
fprintf fmt "@[<v 2>@[TRY %a (loc %a) {@]@;%a@]@;}"
pp_stmt s
pp_cabsloc loc
- (Pretty_utils.pp_list ~sep:"@;" print_one_catch) l
+ (Format.pp_print_list ~pp_sep:Format.pp_print_cut print_one_catch) l
| CODE_ANNOT (_,_) -> fprintf fmt "CODE_ANNOT"
| CODE_SPEC _ -> fprintf fmt "CODE_SPEC"
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 144bb0d584ce4a8f61d9195bd7e4960bd2af9055..c059f8110e4fc104336981b6bc0ffd4f4a933eb8 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -93,10 +93,10 @@ and pp_deps fmt = function
and pp_from fmt = pp_pair pp_identified_term pp_deps fmt
-and pp_assigns pp_locs fmt = function
+and pp_assigns fmt = function
| WritesAny -> Format.fprintf fmt "WritesAny"
| Writes(from_list) ->
- Format.fprintf fmt "Writes(%a)" (pp_list pp_locs) from_list
+ Format.fprintf fmt "Writes(%a)" (pp_list pp_from) from_list
and pp_file fmt file = Format.fprintf fmt "{fileName=%a;globals=%a;globinit=%a;globinitcalled=%a}"
@@ -607,7 +607,8 @@ and pp_location fmt (pos_start,pos_end) =
p fmt "(%a,%a)" pp_filepath_position pos_start pp_filepath_position pos_end
and pp_if_loc_known prefix suffix fmt loc =
- if print_locations && loc <> Cil_datatype.Location.unknown
+ if print_locations &&
+ not (Filepath.Normalized.is_unknown (fst loc).Filepath.pos_path)
then Format.fprintf fmt "%s%a%s" prefix pp_location loc suffix
else ()
@@ -921,7 +922,7 @@ and pp_behavior fmt behavior =
(pp_list pp_identified_predicate) behavior.b_requires
(pp_list pp_identified_predicate) behavior.b_assumes
(pp_list (pp_pair pp_termination_kind pp_identified_predicate)) behavior.b_post_cond
- (pp_assigns pp_from) behavior.b_assigns
+ pp_assigns behavior.b_assigns
pp_allocation behavior.b_allocation
(pp_list pp_acsl_extension) behavior.b_extended
@@ -932,24 +933,30 @@ and pp_termination_kind fmt = function
| Continues -> Format.fprintf fmt "Continues"
| Returns -> Format.fprintf fmt "Returns"
-and pp_loop_pragma pp_term fmt = function
- | Unroll_specs(term_list) -> Format.fprintf fmt "Unroll_specs(%a)" (pp_list pp_term) term_list
- | Widen_hints(term_list) -> Format.fprintf fmt "Widen_hints(%a)" (pp_list pp_term) term_list
- | Widen_variables(term_list) -> Format.fprintf fmt "Widen_variables(%a)" (pp_list pp_term) term_list
+and pp_loop_pragma fmt = function
+ | Unroll_specs(term_list) ->
+ Format.fprintf fmt "Unroll_specs(%a)" (pp_list pp_term) term_list
+ | Widen_hints(term_list) ->
+ Format.fprintf fmt "Widen_hints(%a)" (pp_list pp_term) term_list
+ | Widen_variables(term_list) ->
+ Format.fprintf fmt "Widen_variables(%a)" (pp_list pp_term) term_list
-and pp_slice_pragma pp_term fmt = function
+and pp_slice_pragma fmt = function
| SPexpr(term) -> Format.fprintf fmt "SPexpr(%a)" pp_term term
| SPctrl -> Format.fprintf fmt "SPctrl"
| SPstmt -> Format.fprintf fmt "SPstmt"
-and pp_impact_pragma pp_term fmt = function
+and pp_impact_pragma fmt = function
| IPexpr(term) -> Format.fprintf fmt "IPexpr(%a)" pp_term term
| IPstmt -> Format.fprintf fmt "IPstmt"
-and pp_pragma pp_term fmt = function
- | Loop_pragma(term) -> Format.fprintf fmt "Loop_pragma(%a)" (pp_loop_pragma pp_term) term
- | Slice_pragma(term) -> Format.fprintf fmt "Slice_pragma(%a)" (pp_slice_pragma pp_term) term
- | Impact_pragma(term) -> Format.fprintf fmt "Impact_pragma(%a)" (pp_impact_pragma pp_term) term
+and pp_pragma fmt = function
+ | Loop_pragma(term) ->
+ Format.fprintf fmt "Loop_pragma(%a)" pp_loop_pragma term
+ | Slice_pragma(term) ->
+ Format.fprintf fmt "Slice_pragma(%a)" pp_slice_pragma term
+ | Impact_pragma(term) ->
+ Format.fprintf fmt "Impact_pragma(%a)" pp_impact_pragma term
and pp_assertion_kind fmt = function
| Assert -> Format.pp_print_string fmt "Assert"
@@ -966,12 +973,12 @@ and pp_code_annotation_node fmt = function
Format.fprintf fmt "AVariant(%a)" pp_variant term_variant
| AAssigns(string_list,assigns) ->
Format.fprintf fmt "AAssigns(%a,%a)" (pp_list pp_string) string_list
- (pp_assigns pp_from) assigns
+ pp_assigns assigns
| AAllocation(string_list,allocation) ->
Format.fprintf fmt "AAllocation(%a,%a)" (pp_list pp_string) string_list
pp_allocation allocation
| APragma(pragma) ->
- Format.fprintf fmt "APragma(%a)" (pp_pragma pp_term) pragma
+ Format.fprintf fmt "APragma(%a)" pp_pragma pragma
| AExtended(string_list,is_loop,acsl_extension) ->
Format.fprintf fmt "AExtended(%a,%B,%a)"
(pp_list pp_string) string_list is_loop pp_acsl_extension acsl_extension
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index 7e75af6ca10b138ff880c7179ac847e10024e346..c9f1318b512cc8430d085f7c53b4fb8392bcb099 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -68,9 +68,7 @@ val pp_deps :
Format.formatter -> Cil_types.deps -> unit
val pp_from :
(Cil_types.identified_term * Cil_types.deps) Pretty_utils.formatter
-val pp_assigns :
- Cil_types.from Pretty_utils.formatter ->
- Format.formatter -> Cil_types.assigns -> unit
+val pp_assigns : Format.formatter -> Cil_types.assigns -> unit
val pp_file : Format.formatter -> Cil_types.file -> unit
val pp_global : Format.formatter -> Cil_types.global -> unit
val pp_typ : Cil_types.typ Pretty_utils.formatter
@@ -146,16 +144,12 @@ val pp_behavior : Format.formatter -> Cil_types.behavior -> unit
val pp_termination_kind :
Format.formatter -> Cil_types.termination_kind -> unit
val pp_loop_pragma :
- Cil_types.term Pretty_utils.formatter ->
Format.formatter -> Cil_types.loop_pragma -> unit
val pp_slice_pragma :
- Cil_types.term Pretty_utils.formatter ->
Format.formatter -> Cil_types.slice_pragma -> unit
val pp_impact_pragma :
- Cil_types.term Pretty_utils.formatter ->
Format.formatter -> Cil_types.impact_pragma -> unit
val pp_pragma :
- Cil_types.term Pretty_utils.formatter ->
Format.formatter -> Cil_types.pragma -> unit
val pp_code_annotation_node :
Format.formatter -> Cil_types.code_annotation_node -> unit
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index dff1e2a3fe3004b8b36734f8f06c2559b0b0c3ac..99008be9f2759e59c0896a7f742b8fc4e5175948 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 1cb569973b779f585c25bd11fc53b672c176bf2c..5a166f93f07e86f6225bc60ab3f9edc10a7d8f23 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 1732542c4fd7b93946a1d65c87af05add74d63c3..5ff2f32c9faf813142e4542635f8880f63c82224 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 23bf7d9f478c1f949791c0f1ccdc4e7f6e34a850..cce382d5d4e14eb6c2f28d6bd0c2b66bbce7dcbb 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 65121c53f78759d2e118926a015d4fd24ce0d97f..667d8aeef6ee4b8acc24dc3a74e37ea632197395 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 41cbba0b33f257c87c24b00ca346724f1b4ba4bb..0c436d88610e6560541d59e1fac57c53bd8e30d3 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/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 3b0ee2265e7a1d1ff71f6cd8ae16129411840f89..0714b72b4c9816a4c8a2f4453104fb99bc2fbdab 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -436,17 +436,16 @@ let temp_dir_cleanup_at_exit ?(debug=false) base =
in
try_dir_cleanup_at_exit 10 base
-(* replace "noalloc" with [@@noalloc] for OCaml version >= 4.03.0 *)
-[@@@ warning "-3"]
-external usleep: int -> unit = "ml_usleep" "noalloc"
- (* In ../utils/c_bindings.c ; man usleep for details. *)
-
(* ************************************************************************* *)
(** Strings *)
(* ************************************************************************* *)
-external compare_strings: string -> string -> int -> bool = "compare_strings" "noalloc"
-[@@@ warning "+3"]
+let compare_strings s1 s2 len =
+ try
+ for i = 0 to len - 1 do if s1.[i] <> s2.[i] then raise Exit; done;
+ true
+ with Exit -> false
+ | Invalid_argument _ -> raise (Invalid_argument "Extlib.compare_strings")
let string_prefix ?(strict=false) prefix s =
let add = if strict then 1 else 0 in
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index 6b8084f6922b7696e2566d6d94c14f37d2dbb6ac..50d3745f5506e63bd47700cd3e88dacfe35122c5 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -382,11 +382,6 @@ val safe_remove: string -> unit
val safe_remove_dir: string -> unit
-val usleep: int -> unit
- (** Unix function that sleep for [n] microseconds.
- See [man usleep] for details.
- Should not be used under Win32. *)
-
(* ************************************************************************* *)
(** Comparison functions *)
(* ************************************************************************* *)
diff --git a/src/libraries/stdlib/transitioning.ml.in b/src/libraries/stdlib/transitioning.ml.in
index 779da76ce9aedbc0c12ad68d06cf6dc93938e632..6d95b7a1466454402704bd22f262d9bb770d5096 100644
--- a/src/libraries/stdlib/transitioning.ml.in
+++ b/src/libraries/stdlib/transitioning.ml.in
@@ -78,6 +78,8 @@ module Format = struct
Format.pp_open_@FORMAT_STAG@ fmt s
let pp_close_stag fmt () =
Format.pp_close_@FORMAT_STAG@ fmt ()
+
+ let pp_print_option = @FORMAT_PP_OPT@
end
module Q = struct
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index 03507b2d2cc3ab5497c323f851e3fa94dc3939c7..b07a1d6bd0bb4138a1840dcd60541f3d82d5c720 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -74,6 +74,8 @@ module Format: sig
Format.formatter -> unit -> formatter_stag_functions
val pp_open_stag : Format.formatter -> stag -> unit
val pp_close_stag : Format.formatter -> unit -> unit
+ val pp_print_option: ?none:(Format.formatter -> unit -> unit) ->
+ (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a option -> unit
end
(** {1 Zarith} *)
diff --git a/src/libraries/utils/c_bindings.c b/src/libraries/utils/c_bindings.c
index b03878d2dce1b398d0b097adcbf93c77abdea095..8ca903af5beb0a600e55d2ce00b285e561154172 100644
--- a/src/libraries/utils/c_bindings.c
+++ b/src/libraries/utils/c_bindings.c
@@ -142,13 +142,6 @@ value c_atan2f(value x, value y)
return caml_copy_double(res);
}
-value compare_strings(value v1, value v2, value vlen) {
- if (memcmp(String_val(v1), String_val(v2), Long_val(vlen)) == 0)
- return Val_true;
- else
- return Val_false;
-}
-
value address_of_value(value v)
{
return (Val_long(((unsigned long)v)/sizeof(long)));
@@ -253,9 +246,3 @@ value single_precision_of_string(value str)
double d = f;
return caml_copy_double(d);
}
-
-value ml_usleep(value v)
-{
- usleep( Int_val(v) );
- return Val_unit ;
-}
diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index 45b31c884d839da6ca96f93be61f6e2837d40566..22ab26bbb6a8c694c5244c66eb5762068ce9e68d 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
@@ -259,7 +259,7 @@ let command ?(timeout=0) ?stdout ?stderr cmd args =
| Result r ->
res := r;
false
- in while running () do Extlib.usleep 100000 (* 0.1s *) done ; !res
+ in while running () do Unix.sleepf 0.1 done ; !res
else
let f = command_generic ~async:false ?stdout ?stderr cmd args in
match f () with
diff --git a/src/libraries/utils/task.ml b/src/libraries/utils/task.ml
index 6dd5eb96cff7cf274d3bffcaab2e9ec22eceb6ae..164a847defba67d1c9dbdbe964127a9f570c01fb 100644
--- a/src/libraries/utils/task.ml
+++ b/src/libraries/utils/task.ml
@@ -109,7 +109,8 @@ struct
let rec wait = function
| UNIT a -> a
| YIELD f -> Db.yield() ; wait (f Coin)
- | WAIT(ms,f) -> Db.yield() ; Extlib.usleep ms ; wait (f Coin)
+ | WAIT(ms,f) ->
+ Db.yield() ; Unix.sleepf (float_of_int ms /. 1_000_000.); wait (f Coin)
let finished = function UNIT a -> Some a | YIELD _ | WAIT _ -> None
@@ -341,7 +342,7 @@ let share sh = todo
let on_idle = ref
(fun f -> try
- while f () do Extlib.usleep 50000 (* wait for 50ms *) done
+ while f () do Unix.sleepf 0.05 (* wait for 50ms *) done
with Db.Cancel -> ())
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 8c8c16416f640b15fed479adb985a2ac1f438017..dee262fbb103a770705562d9d87c67640e7fc524 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 22d070fd84b672e3022e99cb8528ca0850cc8b98..69b3c42024f18b6584c06ef03d58eea1b1fa78fd 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 48b2b6d40bd5c64b83a0fedb52cbbb0d14d88a6f..298d75d184f3a4716f4ba7573be412659061ef06 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 0156c2030ffbfaad86377aa571256d9d4f3820e6..68983f58f9e9e87bfba191d367b1426cad105654 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 dd043d7b74e59666751c1c51b09e880e8bf0d875..f3e3ed9226d9aefc42ce456d75c9be0db374004c 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 c1492a8c3ba77b74c1d4d45bb02661ce19211498..539a3f6376782a6d764193a6a1e9b740513e8f68 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 82fb8d6d0fc9bb96b506b7da70292f65a7fc4d2c..ba15f820bfa17c098dc679eefd7155835e427a06 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 d91eedd7885452a4d41875defa1deabe905c8866..cab11780aec9205349d18ca0595ccef333d7fcd3 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 fefac22423607ff9ef39fd6cb37d8d99426a4f72..22866e37d795837bb857aaac923f27cea03de156 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 688f33b7f985925fdcd3f265be9146da7c444275..2558f8efefb71f7428c8f15d781296edcaa0858e 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 4948f0892dec9e05ab496f3e4d7e48fc98ae59de..e3c5407e4b424514569cfb508b3255d56159da89 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 ef58b57e3e7619374437321b9e7b351a194b611f..f8d633e00f26790179bcfd45964646ac62c1a1ca 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 b99a36febdc539564f1c7a0409f008c4df06519e..509dbcb3e7b582fa822dc615dc4d4cf3802d41c0 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 8202d68da17708e332dee875e8a47747f1e15370..219694d2e8f0dc6aa4ca8ac2f483363d67b3e970 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 ce69f25c601c328fdde8185f26d6a87ccc7d4e4f..6fa7f52646edde6a534679816ff750640fffbb95 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 2105830a936e06aa098150218820272fab0a82b7..c51486acaecd1ccf588f1180f59d1728c5a81768 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