diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 06d9e223bd630d88959d5f81bc10340beb855627..61cfff6e8f372025902928a1921cd3a13bfd8e26 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -106,9 +106,8 @@ used, it is possible to have logic identifiers with an extended lexical format:
For instance, \verb+Foo::bar'jazz+ is a syntactically valid identifier.
\end{itemize}
-There is currently no support for external specification loaders from the
-standard distribution of \FramaC, although external plug-ins might define some
-using the extension API, consult the plug-in developer manual for details.
+External module loaders are defined by plug-ins \textit{via} the extension API,
+consult the plug-in manuals and the plug-in developer manual for more details.
%%% Local Variables:
%%% mode: latex
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index bbaecca93d1a04a4108183b023200631450dc8a0..03fcf36d93d0dc7b99499eb80008da9a71a7cf57 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,7 @@
Plugin WP <next-release>
###############################################################################
+- WP [2024-09-24] Why3 module importer (See manual § 2.4.13)
- WP [2024-09-13] -wp-par now defaults to the number of logical cores
-! WP [2024-08-23] Remove wp_region
-* WP [2024-07-02] Fixed parsing of decimal literals
diff --git a/src/plugins/wp/doc/.gitignore b/src/plugins/wp/doc/.gitignore
index bfe2e4d25500d764b549b9e6dfd00ae71d137617..28c4dfcc0ceb3c64c16e16bd9784bf716063f224 100644
--- a/src/plugins/wp/doc/.gitignore
+++ b/src/plugins/wp/doc/.gitignore
@@ -3,3 +3,4 @@ frama-c-affiliation.tex
cealistlogo.jpg
feedback
/html
+/manual/wp.synctex.gz
diff --git a/src/plugins/wp/doc/manual/wp_builtins.tex b/src/plugins/wp/doc/manual/wp_builtins.tex
index 5c04a947a4d802c007d8814f5814ba2cb43a10ad..6a98a84396319b1367bd7633dbfd8b1561ea04d7 100644
--- a/src/plugins/wp/doc/manual/wp_builtins.tex
+++ b/src/plugins/wp/doc/manual/wp_builtins.tex
@@ -247,6 +247,9 @@ $x$ and $y$ are finite, but obey IEEE semantics for infinities and NaNs
\section{Custom Extensions}
+\paragraph{DEPRECATED.} You shall import a Why3 module instead of using custom
+drivers. See Section~\ref{importer} for details.
+
As explained in Section~\ref{drivers}, it is possible to extend all the properties mentioned
above. Section~\ref{wp-custom-tactics} also provides hints on how to define tactics that can be
used in the interactive prover of \textsf{Frama-C/WP}.
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index c2a27e1a29737f1ddcf0eb77f4640726acb44c94..591e53d48010d8780c31aee5526725118e288b61 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1651,6 +1651,9 @@ procedures thanks to the following option:
\subsection{Linking \textsf{ACSL} Symbols to External Libraries}
\label{drivers}
+\paragraph{DEPRECATED.} You shall now import a Why3 module
+instead of using custom drivers. See Section~\ref{importer} for details.
+
Besides additional proof libraries, it is also possible to
\emph{link} declared \textsf{ACSL} symbols to external or predefined
symbols. In such case, the corresponding \textsf{ACSL} definitions,
@@ -1660,7 +1663,6 @@ External linkage is specified in \emph{driver files}. It is possible
to load one or several drivers with the following \textsf{WP} plug-in option:
\begin{description}
\item[\tt -wp-driver <file,\ldots>] load specified driver files.
-
\end{description}
\newcommand{\ccc}{\texttt{,}\ldots\texttt{,}}
@@ -1782,6 +1784,48 @@ by a link (`\user{link};'). The available tags are depicted on figure~\ref{wp-dr
\label{wp-driver-tags}
\end{figure}
+\pagebreak
+\subsection{Importing Why3 Modules}
+\label{importer}
+
+The \textsf{WP} plug-in provides an \textsf{ACSL} module loader that
+can import \textsf{Why3} theories and modules into \textsf{ACSL}.
+See \textsf{Frama-C} user manual, Section § 6.3 for details.
+Here is an example of use:
+
+\begin{lstlisting}
+//@ import why3: number::Gcd;
+
+/*@
+ assigns \nothing;
+ ensures \result == Gcd::gcd(a,b);
+*/
+int euclid(int a, int b)
+{
+ int r;
+ /*@
+ loop assigns a, b, r;
+ loop invariant Gcd::gcd(a,b) == \at( Gcd::gcd(a,b), Pre );
+ loop variant \abs(b);
+ */
+ while( b != 0 ) {
+ r = b ;
+ b = a % b ;
+ a = r ;
+ }
+ return a < 0 ? -a : a;
+}
+\end{lstlisting}
+
+\noindent
+The Why3 load-path can be specified from the command-line:
+\begin{description}
+ \item[\tt -wp-library <dir,\ldots>] add the specified directory to the Why3 load-path.
+\end{description}
+
+\noindent
+Notice that the Why3 standard library is already in the load-path by default.
+
\clearpage
\subsection{Proof Session \& Cache}
\label{wp-cache}
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index efb064a639de06c19ba50ed0590885f962904aac..2c4c8f714efe74909d4f016b14f631da0369dfbb 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -751,17 +751,6 @@ module Tactics = String_list
let () = on_reset Tactics.clear
let () = Parameter_customize.set_group wp_prover
-let () = Parameter_customize.is_invisible ()
-module Import =
- String_list
- (struct
- let option_name = "-wp-import"
- let arg_name = "thy,..."
- let help = "Import Why3 theories"
- end)
-
-let () = Parameter_customize.set_group wp_prover
-let () = Parameter_customize.is_invisible ()
module Library =
Filepath_list
(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 84a25a418c36a8b3ca43d84f4b195aeb76505873..1a0da8692295a6e2a8b524dd9928284ec09f13f6 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -116,7 +116,6 @@ module Cache: Parameter_sig.String
module CacheEnv: Parameter_sig.Bool
module CacheDir: Parameter_sig.String
module CachePrint: Parameter_sig.Bool
-module Import: Parameter_sig.String_list
module Library: Parameter_sig.Filepath_list
module Drivers: Parameter_sig.Filepath_list
module Timeout: Parameter_sig.Int