diff --git a/bin/dune b/bin/dune
index fcb02ca1875c5cb8ee96640a75302a745c1f3261..7e3bb9f33bdda4cb426fda2c8128a406b985c95b 100644
--- a/bin/dune
+++ b/bin/dune
@@ -27,5 +27,6 @@
(frama-c-script as frama-c-script)
(frama-c-config as frama-c-config)
(test.sh as frama-c-test.sh)
+ (frama-c-build-scripts.sh as frama-c-build-scripts.sh)
)
)
diff --git a/bin/frama-c-build-scripts.sh b/bin/frama-c-build-scripts.sh
new file mode 100755
index 0000000000000000000000000000000000000000..d0698b6bf81350bf0bdde2431dbe4446e2a54f6e
--- /dev/null
+++ b/bin/frama-c-build-scripts.sh
@@ -0,0 +1,194 @@
+#!/bin/bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# 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). #
+# #
+##########################################################################
+
+PACKAGE="frama-c-scripts"
+
+CMD="init"
+
+THIS_SCRIPT="$0"
+Usage () {
+ echo "Usage: $(basename ${THIS_SCRIPT}) [<command>] [options] <script-dir> [<modules>]"
+ echo " Build a script library to be used by Frama-C kernel."
+ echo ""
+ echo "Commands:"
+ echo "- init: generates dune files (default command)"
+ echo "- build: performs the compilation of the script libraries via \"dune build @install\""
+ echo "- install: performs the installation of the script libraries via \"dune install\""
+ echo ""
+ echo "Options:"
+ echo " -help: prints usage information"
+ echo " -package-name <name>: set the <name> of the package of the libraries (defaults to \"${PACKAGE}\")."
+ echo " note: once the dune-project file has been created, don't set another name."
+ echo ""
+ echo "Arguments:"
+ echo " <script-dir>: directory that contents the script files:"
+ echo " - the basename of this directory fixes the name of the script library: ${PACKAGE}.<basename>"
+ echo " - a 'dune' file is created (if it does not exists before) into this directory"
+ echo " - a 'dune-project' file is created (if it does not exists before) into the parent directory"
+ echo " - note: the parent directory is './' when the script directory is also './'"
+ echo " <modules>: names of the OCaml modules that compose the script (default to all OCaml modules of the script directory)"
+}
+
+Error () {
+ echo "Error: $@"
+ Usage
+ exit 1
+}
+
+###############
+# Command line processing
+
+case "$1" in
+ "init"|"build"|"install") CMD="$1"; shift;;
+ *) ;;
+esac
+
+while [ "$1" != "" ]; do
+ case "$1" in
+ "-package-name") shift ; PACKAGE="$1";;
+ "-h"|"-help"|"--help") Usage; exit 0;;
+ *) break ;;
+ esac
+ shift
+done
+
+[ "$PACKAGE" != "" ] || Error "Missing option value: no package name"
+[ "$1" != "" ] || Error "Missing argument: no script directory"
+
+SCRIPT_DIR="$1"
+shift
+SCRIPT_FILES="$@"
+SCRIPT_LIBS=""
+
+[ -d "${SCRIPT_DIR}" ] || Error "Missing script directory: ${SCRIPT_DIR})"
+
+###############
+
+DuneProject () {
+ echo "(lang dune 3.0)"
+ echo "(generate_opam_files true)"
+ echo "(name ${PACKAGE})"
+ echo "(maintainers \"anonymous\")"
+ echo "(package (name ${PACKAGE})"
+ echo " (depends"
+ echo " (\"frama-c\" (>= 26.0))"
+ echo " )"
+ echo " (tags (\"Frama-C scripts\"))"
+ echo ")"
+}
+
+Dune () {
+ echo "(rule"
+ echo " (alias ${PACKAGE})"
+ echo " (deps (universe))"
+ echo " (action (echo \"- Script ${SCRIPT_NAME}:\" %{lib-available:${PACKAGE}.${SCRIPT_NAME}} \"\\\\n\"))"
+ echo ")"
+ echo ""
+ echo "(library"
+ echo " (name ${SCRIPT_NAME})"
+ echo " (optional)"
+ echo " (public_name ${PACKAGE}.${SCRIPT_NAME})"
+ [ "${SCRIPT_FILES}" = "" ] || echo " (modules ${SCRIPT_FILES})"
+ echo " (flags -open Frama_c_kernel :standard -w -9)"
+ echo " (libraries frama-c.kernel ${SCRIPT_LIBS})"
+ echo ")"
+}
+
+###############
+
+GenerateFile () {
+ if [ -e "$2" ]; then
+ echo "$1 file exists already: $2"
+ else
+ echo "- Creating $1 file: $2"
+ $1 | while read p; do
+ echo "$p" >> "$2"
+ done
+ fi
+}
+
+###############
+
+SCRIPT_NAME="$(basename "${SCRIPT_DIR}")"
+DUNE_PROJECT_DIR="$(dirname "${SCRIPT_DIR}")"
+DUNE_PROJECT="${DUNE_PROJECT_DIR}/dune-project"
+case "${SCRIPT_DIR}" in
+ */) DUNE_FILE="${SCRIPT_DIR}dune" ;;
+ *) DUNE_FILE="${SCRIPT_DIR}/dune" ;;
+esac
+
+###############
+
+EchoDuneCmd() {
+ if [ "${DUNE_PROJECT_DIR}" = "." ]; then
+ echo " > $@"
+ else
+ echo " > (cd ${DUNE_PROJECT_DIR} && $@)"
+ fi
+}
+
+DuneBuild() {
+ echo ""
+ echo "- Compiling the script library \"${PACKAGE}.${SCRIPT_NAME}\" via \"dune build @install\" command..."
+ dune build @install
+ [ "$?" = "0" ] || Error "the compilation fails!"
+}
+
+DuneInstall() {
+ echo ""
+ echo "- Install the script library \"${PACKAGE}.${SCRIPT_NAME}\" via \"dune install\" command..."
+ dune install
+}
+
+###############
+
+[ "$(basename "${DUNE_FILE}")" = "dune" ] || Error "Wrong basename for a dune file: ${DUNE_FILE}"
+[ "$(basename "${DUNE_PROJECT}")" = "dune-project" ] || Error "Wrong basename for a dune-project file: ${DUNE_PROJECT}"
+
+GenerateFile DuneProject "${DUNE_PROJECT}"
+GenerateFile Dune "${DUNE_FILE}"
+
+if [ "$CMD" = "init" ]; then
+ echo ""
+ echo "To compile the all scripts defined inside this 'dune project' \"${PACKAGE}\", runs the following command:"
+ EchoDuneCmd "dune build @install"
+else
+ DuneBuild
+fi
+echo ""
+echo "So, the script libraries, are compiled and installed into the local '_build' directory."
+echo "That also create or update the 'opam' file \"${PACKAGE}.opam\" allowing a global installation of all script libraries."
+echo ""
+echo "To load this script library from Frama-C, runs the following command:"
+EchoDuneCmd "dune exec -- frama-c -load-library ${PACKAGE}.${SCRIPT_NAME} ..."
+
+if [ "$CMD" = "install" ]; then
+ DuneInstall
+else
+ echo ""
+ echo "All libraries of this 'dune project' \"${PACKAGE}\" can also be installed via 'dune' using from the generated 'opam' file: \"${PACKAGE}.opam\""
+ EchoDuneCmd "dune install"
+fi
+echo ""
+echo "Then, this script library can directly be loaded by Frama-C from the following command:"
+echo " > frama-c -load-library ${PACKAGE}.${SCRIPT_NAME} ..."
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index faf704b58d7f19724efc38cd906013b9ebefb140..a57e0d3ed55d8bf6a0b5e6723a1478d09ae32319 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -133,7 +133,7 @@ let load_module m =
let base,ext = split_ext m in
match ext with
| ".ml" ->
- Klog.error "Script loading as been deprecated in favor of the command frama-c-init-plugin"
+ Klog.error "Script loading as been deprecated in favor of the load of script libraries (see shell script `frama-c-build-scripts.sh` to build such a script library that can be loaded via the Frama-C option `-load-library`)."
| _ ->
begin
(* load object or compile script or find package *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index b78902d70ec4d0111ba1d7dcf03900a09e8fef4b..a45fb58818fb1880d2fffdf7e4db4fe74d6b460c 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -868,11 +868,23 @@ module LoadModule =
let option_name = "-load-module"
let module_name = "LoadModule"
let arg_name = "SPEC,..."
- let help = "Dynamically load modules and scripts. \
- Each <SPEC> can be an OCaml source or object file, with \
+ let help = "Dynamically load modules. \
+ Each <SPEC> can be object file, with \
or without extension, or a Findlib package. \
- Loading order is preserved and \
- additional dependencies can be listed in *.depend files."
+ Loading order is preserved, but after plugins and libraries."
+ end)
+
+let () = Parameter_customize.set_group saveload
+let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
+let () = Parameter_customize.do_not_projectify ()
+module LoadLibrary =
+ String_list
+ (struct
+ let option_name = "-load-library"
+ let module_name = "LoadLibrary"
+ let arg_name = "<libname,..."
+ let help = "Dynamically load libraries. \
+ Loading order is preserved, but the load is done between the plugins and the modules."
end)
let () = Parameter_customize.set_group saveload
@@ -903,6 +915,7 @@ let bootstrap_loader () =
begin
if AutoLoadPlugins.get () then Dynamic.load_plugin_path () ;
List.iter Dynamic.load_plugin (LoadPlugin.get()) ;
+ Dynamic.load_packages (LoadLibrary.get()) ;
List.iter Dynamic.load_module (LoadModule.get()) ;
end
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index fbf977acbe0b2309ae4df4f109cff9273b77a780..4937534d6ea3de301c5c750b460441872f34ec98 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -372,6 +372,11 @@ module LoadState: Parameter_sig.Filepath
module LoadModule: Parameter_sig.String_list
(** Behavior of option "-load-module" *)
+module LoadLibrary: Parameter_sig.String_list
+(** Behavior of option "-load-library"
+ @since Frama-C+dev
+*)
+
module AutoLoadPlugins: Parameter_sig.Bool
(** Behavior of option "-autoload-plugins" *)