Commit aedae7e6 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[config] change name of config.ml to avoid clash with compiler internal lib

parent e8de7b00
......@@ -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
......
......@@ -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) $@
......
#! /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
......@@ -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",
......
......@@ -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"
......
......@@ -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 () =
......
......@@ -20,4 +20,4 @@
(* *)
(**************************************************************************)
let () = Topdirs.dir_directory Config.libdir
let () = Topdirs.dir_directory Fc_config.libdir
......@@ -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
......
......@@ -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;
......
......@@ -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
......
......@@ -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 -> []
......
......@@ -25,7 +25,6 @@
(* ************************************************************************* *)
module CamlString = String
module Fc_config = Config
let () = Plugin.register_kernel ()
......
......@@ -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)
......
......@@ -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
......
......@@ -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
......
......@@ -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));*)
......
......@@ -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) ||
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment