diff --git a/bin/dune b/bin/dune index a1b9696649bc795b6c2b11f8e6c45cbbb2b8d2e1..86b17794f21410b22618a8241a29120928303930 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 7f755097168009016c2ba0efca80f10cdadad62b..e71ca6ebe7d600ed09ca9fbe5786cf66dd824e13 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 bb5cc2ad54066c0565c519c04059ed50e0034863..2fe427c9796cfb58bf9c3106c2708eedc68cffbb 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 d0725968ca6a4ee86f8e55e488717ec95f0152d3..c22104e8bb3e63318a717c3a8e6c0e74dba9d8ec 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 fe20f1848549c440da0d6a57421e2dd2ac1639f3..c984ba9a656af3eedaf32ed24e6f75928d4fd438 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 *)