From 68c135522b987a4f7e9815c5ad4b793ff9a9a8e8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 16 Apr 2024 16:43:38 +0200
Subject: [PATCH] [Dev] remove frama-c-build-scripts.sh and document
alternative
---
bin/dune | 1 -
dev/set-dune-version.sh | 1 -
dev/set-version.sh | 3 --
doc/userman/user-plugins.tex | 37 +++++++++++++++++++
.../plugin_entry_points/dynamic.ml | 2 +-
5 files changed, 38 insertions(+), 6 deletions(-)
diff --git a/bin/dune b/bin/dune
index a1b9696649b..86b17794f21 100644
--- a/bin/dune
+++ b/bin/dune
@@ -27,6 +27,5 @@
(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/dev/set-dune-version.sh b/dev/set-dune-version.sh
index 7f755097168..e71ca6ebe7d 100755
--- a/dev/set-dune-version.sh
+++ b/dev/set-dune-version.sh
@@ -43,7 +43,6 @@ fi
find . -name dune-project -exec $SED -i -e "s/(lang dune [1-9]\.[0-9]*)/(lang dune ${VERSION})/gI" '{}' ';'
find . -name dune-workspace.* -exec $SED -i -e "s/(lang dune [1-9]\.[0-9]*)/(lang dune ${VERSION})/gI" '{}' ';'
-$SED -i -e "s/(lang dune [1-9]\.[0-9]*)/(lang dune ${VERSION})/gI" ./bin/frama-c-build-scripts.sh
echo "All dune-project related files have been updated".
echo "Remember to update:"
diff --git a/dev/set-version.sh b/dev/set-version.sh
index bb5cc2ad540..2fe427c9796 100755
--- a/dev/set-version.sh
+++ b/dev/set-version.sh
@@ -125,9 +125,6 @@ else
$SED -i "s/\(^\\\\section\*{E-ACSL \\\\eacslpluginversion \\\\eacslplugincodename}\)/%\1\n\n\\\\section\*{E-ACSL $NEXT_MAJOR.$NEXT_MINOR $NEXT_CODENAME}/g" \
src/plugins/e-acsl/doc/userman/changes.tex
- # Frama-C build script
- $SED -i "s/(\\\\\\\"frama-c\\\\\\\" (>= [1-9][0-9]\.[0-9]))/(\\\\\\\"frama-c\\\\\\\" (>= $NEXT_MAJOR.$NEXT_MINOR))/g" bin/frama-c-build-scripts.sh
-
# Reference configuration
$SED -i "s/Frama-C [1-9][0-9]\.[0-9]/Frama-C $NEXT_MAJOR.$NEXT_MINOR/gI" \
reference-configuration.md
diff --git a/doc/userman/user-plugins.tex b/doc/userman/user-plugins.tex
index d0725968ca6..c22104e8bb3 100644
--- a/doc/userman/user-plugins.tex
+++ b/doc/userman/user-plugins.tex
@@ -58,6 +58,43 @@ installation. Loading will fail and a warning will be emitted at launch if this
is not the case.
\end{important}
+\subsection{Loading Single OCaml Files as Plug-ins}
+
+\FramaC used to have an option \texttt{-load-script} that allowed loading a
+single OCaml file as a mini-plug-in. Since \FramaC 26 (Iron), the use of Dune
+requires a different approach: you need to create a directory containing the
+following files:
+\begin{itemize}
+\item a \texttt{dune-project} file;
+\item a \texttt{dune} file;
+\item the \texttt{script.ml} file that you want to load with \FramaC.
+\end{itemize}
+With these files, you will be able to run \texttt{dune build} to compile the
+script, and then \texttt{frama-c -load-module script.cmxs} to load it.
+
+Here is an example \texttt{dune-project} file:
+\begin{dunecode}
+(lang dune 3.7)
+\end{dunecode}
+
+Note: you can match the language version (here, 3.7) to the one of your
+installed \texttt{dune} package. Later versions often enable additional
+warnings.
+
+Here is an example \texttt{dune} file:
+\begin{dunecode}
+(executable
+ (name "script") ; must match the name of the .ml file
+ (modes plugin)
+ (libraries frama-c.init.cmdline frama-c.kernel) ; add more if needed
+ (flags -open Frama_c_kernel :standard)
+ (promote (until-clean)) ; keeps script.cmxs in the base directory
+)
+\end{dunecode}
+
+If your script depends on \FramaC plug-ins, you need to add them to
+\texttt{libraries}, e.g. \texttt{frama-c-<plugin>.core}.
+
% Local Variables:
% ispell-local-dictionary: "english"
% TeX-master: "userman.tex"
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index fe20f184854..c984ba9a656 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -129,7 +129,7 @@ let load_module m =
let base,ext = split_ext m in
match ext with
| ".ml" ->
- Klog.error "Script loading has 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`)."
+ Klog.error "Script loading has been deprecated in favor of the load of script libraries (see section \"Loading Single OCaml Files as Plug-ins\" in the Frama-C user manual for an alternative)."
| _ ->
begin
(* load object or compile script or find package *)
--
GitLab