diff --git a/Makefile b/Makefile index da2148f462a8ead5283e7a45c8b6c7ee55c6606a..229bb16d7d40fd5eadeb540bcdcf6e215f01952a 100644 --- a/Makefile +++ b/Makefile @@ -87,7 +87,7 @@ MAJOR_VERSION=$(shell $(SED) -E 's/^([0-9]+)\..*/\1/' VERSION) MINOR_VERSION=$(shell $(SED) -E 's/^[0-9]+\.([0-9]+).*/\1/' VERSION) VERSION_CODENAME=$(shell $(CAT) VERSION_CODENAME) -config.sed: VERSION share/Makefile.config Makefile configure.in +config.sed: VERSION share/Makefile.config share/Makefile.common Makefile configure.in @echo "# generated file" > $@ @echo "s|@VERSION_CODENAME@|$(VERSION_CODENAME)|" >> $@ @echo "s|@VERSION@|$(VERSION)|" >> $@ diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index 1be1e161e81026b4b4d255c1605fdd11f083defa..ec3495ce12299cdb96f841ccb62814c8e44611b2 100644 --- a/doc/developer/advance.tex +++ b/doc/developer/advance.tex @@ -3214,8 +3214,7 @@ their execution order. \begin{enumerate}[(a)] \item the command line options registered for the \texttt{Cmdline.Extending}\sscodeidxdef{Cmdline}{stage}{Extending} stage - are treated, such as \texttt{-load-script} and - \texttt{-add-path}; + are treated, such as \texttt{-load-script} \item the hooks registered through \texttt{Cmdline.run\_during\_extending\_stage} diff --git a/man/frama-c.1.md b/man/frama-c.1.md index 30c76c5d3c59430a1b1abd0ea0661a02d708e008..0101d8c0675454a52e81506aced9137881e7753c 100644 --- a/man/frama-c.1.md +++ b/man/frama-c.1.md @@ -81,10 +81,6 @@ This option has the same per-plugin (and kernel) specializations as Bounds are parsed as OCaml integer constants. By default, all numerical addresses are considered invalid. --add-path *p1[,p2[...,pn]]* -: adds directories *p1* through *pn* to the list of directories in which -plugins are searched. - [-no]-aggressive-merging : merges function definitions modulo renaming. Defaults to no. @@ -530,10 +526,6 @@ the following variables. FRAMAC_LIB : The directory where kernel's compiled interfaces are installed. -FRAMAC_PLUGIN -: The directory where Frama-C can find standard plugins. -If you wish to have plugins in several places, use **-add-path** instead. - FRAMAC_SHARE : The directory where Frama-C data (e.g. its version of the standard library) is installed. diff --git a/share/Makefile.common b/share/Makefile.common index affc77563611993266375cc54d2dfdfb7d31ba4e..d62520b26de85f9a2d47080473fbeabdfd5f5bef 100644 --- a/share/Makefile.common +++ b/share/Makefile.common @@ -87,7 +87,7 @@ ifeq ($(DEVELOPMENT),yes) # - 67 (unused module parameter in functor signature): naming all parameters # in functor signatures is a common practice that seems harmless. Warning 60 # ensures that named functor parameters are indeed used in the implementation. -WARNINGS ?= -w +a-4-6-9-40-41-42-44-45-48-50-67 +WARNINGS ?= +a-4-6-9-40-41-42-44-45-48-50-67 # - 3 (deprecated feature) cannot always be avoided for OCaml stdlib when # supporting several OCaml versions @@ -105,7 +105,7 @@ WARN_ERROR ?= -warn-error +a-3-4-32-33-34-35-36-37-38-39-58 else -WARNINGS ?= -w -a +WARNINGS ?= -a endif #DEVELOPMENT diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml index 24b0a8fd54607c725024d38874e17f66e716383f..d6523cf567646be8e5eebdda75f68fd6ee29d58f 100644 --- a/src/kernel_services/plugin_entry_points/dynamic.ml +++ b/src/kernel_services/plugin_entry_points/dynamic.ml @@ -131,59 +131,22 @@ let load_packages pkgs = let load_script base = Klog.feedback ~dkey "compiling script '%s.ml'" base ; - let cmd = Buffer.create 80 in - let fmt = Format.formatter_of_buffer cmd in - begin - if Dynlink.is_native then - Format.fprintf fmt "ocamlfind ocamlopt -shared -o %S.cmxs" base - else - Format.fprintf fmt "ocamlfind ocamlc -c"; - Format.fprintf fmt " -package frama-c.kernel -open Frama_c_kernel -g %s -warn-error a" Fc_config.ocaml_wflags ; - if Fc_config.is_gui then Format.pp_print_string fmt " -package lablgtk2" ; - Format.fprintf fmt " %s.ml" base ; - Format.pp_print_flush fmt () ; - let cmd = Buffer.contents cmd in - Klog.feedback ~dkey "running '%s'" cmd ; - begin - let res = Sys.command cmd in - if res <> 0 - then Klog.error "compilation of '%s.ml' failed" base - else - let pkg = Filename.basename base in - if Dynlink.is_native then - dynlib_module pkg (base ^ ".cmxs") - else - dynlib_module pkg (base ^ ".cmo") ; - end ; - let erase = Printf.sprintf "rm -f %s.cm* %s.o" base base in - Klog.feedback ~dkey "running '%s'" erase ; - let st = Sys.command erase in - if st <> 0 then - Klog.warning "Error when cleaning '%s.[o|cm*]' files" base ; - end + let result, stdout, stderr = + Dune_site_plugins.V1.load_script + ~open_:["Frama_c_kernel"] + ~warnings:Fc_config.ocaml_wflags + (base^".ml") + in + List.iter (Format.printf "%s") stdout; + List.iter (Format.eprintf "%s") stderr; + match result with + | `Ok -> () + | `Compilation_failed -> Klog.error "compilation of '%s.ml' failed" base (* -------------------------------------------------------------------------- *) (* --- Command-Line Entry Points --- *) (* -------------------------------------------------------------------------- *) -(* See https://github.com/ocaml/dune/pull/636 about why the path separator for - ocamlfind is ';' on Cygwin. *) -let ocamlfind_path_separator = if Sys.cygwin || Sys.win32 then ";" else ":" - -let set_module_load_path path = - let check_dir ~user d = - if is_dir d then true else - ( if user then Klog.warning "cannot load '%s' (not a directory)" d - ; false ) in - let paths = - [List.filter (check_dir ~user:true) path; - (if Fc_config.is_gui then Config_data.Plugins.Plugins_gui.paths else []); - Config_data.Plugins.Plugins.paths] in - let ocamlpath = (String.concat ":" (List.flatten paths)) in - (* Unix.putenv "OCAMLPATH" ocamlpath; (\* for script *\) *) - Klog.debug ~dkey "setting findlib path to %s" ocamlpath - (* Config_data.Plugins.Plugins. .init paths () *) - let load_plugin_path () = if Fc_config.is_gui then Config_data.Plugins.Plugins_gui.load_all (); Config_data.Plugins.Plugins.load_all () diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli index dc0947a0a3aab57ad0ba3d01c4865c7709e8474a..8099335c8596c10b619b2f5d477e122ac424d662 100644 --- a/src/kernel_services/plugin_entry_points/dynamic.mli +++ b/src/kernel_services/plugin_entry_points/dynamic.mli @@ -155,12 +155,6 @@ val load_module: string -> unit val load_plugin: string -> unit -(** Sets the load path for modules in FRAMAC_PLUGIN, prepending it with [path]. - Does not load any plugins. - Must be invoked only once from boot during extending stage. - @since Phosphorus-20170501-beta1. *) -val set_module_load_path : string list -> unit - (**/**) val load_plugin_path: unit -> unit (** Load all plugins in the path set with [set_module_load_path]. diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index d042cacf5d5569d50b78e4cceb09ab119e8f3c8d..d6d67a3a824a65194cc5fc5c82defeb7d68d628d 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -787,18 +787,6 @@ module LoadState = let help = "load a previously-saved session from file <filename>" end) -let () = Parameter_customize.set_group saveload -let () = Parameter_customize.set_cmdline_stage Cmdline.Extending -let () = Parameter_customize.do_not_projectify () -module AddPath = - String_list - (struct - let option_name = "-add-path" - let module_name = "AddPath" - let arg_name = "DIR,..." - let help = "Prepend directories to FRAMAC_PLUGIN for loading dynamic plug-ins" - end) - let () = Parameter_customize.set_group saveload let () = Parameter_customize.set_cmdline_stage Cmdline.Extending let () = Parameter_customize.do_not_projectify () @@ -842,7 +830,6 @@ module AutoLoadPlugins = let bootstrap_loader () = begin - Dynamic.set_module_load_path (AddPath.get ()); if AutoLoadPlugins.get () then Dynamic.load_plugin_path () ; List.iter Dynamic.load_plugin (LoadPlugin.get()) ; List.iter Dynamic.load_module (LoadModule.get()) ; diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index fe84dce4a7fd578c342bc564dcb4f41bdabdbcfd..3736837fa8cfba68b6675278c63dcd4baa1af5e7 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -672,15 +672,6 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then `test -f "$DEVELOPMENT/META.frama-c-e_acsl" -o \ -f "$FRAMAC_PLUGIN/META.frama-c-e_acsl"; echo $?` EACSL_SHARE="$DEVELOPMENT/share/e-acsl" - # Add the project directory to FRAMAC_PLUGINS, - # otherwise Frama-C uses an installed version - if test -f "$DEVELOPMENT/META.frama-c-e_acsl"; then - FRAMAC_FLAGS="-add-path=$DEVELOPMENT/top -add-path=$DEVELOPMENT $FRAMAC_FLAGS"; - fi -else - # Installed version. FRAMAC_SHARE should not be used here as Frama-C - # and E-ACSL may not be installed to the same location - EACSL_SHARE="$BASEDIR/../share/frama-c/e-acsl/" fi # Architecture-dependent flags. Since by default Frama-C uses 32-bit diff --git a/tests/dynamic/dynamic.i b/tests/dynamic/dynamic.i index f0c2034cf824212889789b0d37c7f8c367b2859a..f8ce8665d480304a6887733170853ca602fd23ab 100644 --- a/tests/dynamic/dynamic.i +++ b/tests/dynamic/dynamic.i @@ -1,5 +1,4 @@ /*run.config CMXS: empty abstract abstract2 - OPT: -add-path file_path -add-path directory_path -add-path none OPT: -load-module %{dep:empty.cmxs},%{dep:abstract.cmxs},%{dep:abstract2.cmxs} */