From 4938f1c740368c5baf1cc1d25a1d2bf7edb563f5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 20 Aug 2024 10:35:58 +0200
Subject: [PATCH] [modules] move doc to devman
---
doc/developer/advance.tex | 49 +++++++++++++++++++++++++++++++++------
doc/userman/user-acsl.tex | 48 +++-----------------------------------
2 files changed, 45 insertions(+), 52 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index cd83ca86c6..3a90d0e503 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -4120,22 +4120,33 @@ version in the interface:
\paragraph{External Modules.}
\label{par:ext-modules}
+
Finally, let us introduce how to extend \acsl
modules with external module importers. A typical usage is to import logical
definitions from other languages, e.g. \textsf{Coq} or \textsf{Why3}, as regular
\acsl module definitions. From the user point the view, this takes the form
of an extended \verb+import+ clause:
+\begin{lstlisting}
+//@ import <loader>: <module-name> [ \as <alias-name> ];
+\end{lstlisting}
+
+The syntax is similar to the geneal \verb+import+ annotation, except that the
+module name is prefixed with the name of the loader extension. For instance:
+
\begin{lstlisting}[style=c]
//@ \import Foo: foo::bar::Jazz ;
\end{lstlisting}
Here, \verb+Foo:+ specifies the name of the \acsl extension responsible for
importing the module, and \verb+foo::bar::Jazz+ is the name of the module
-to be imported. To register such an \acsl extension point, a plug-in shall call
-the \verb+Acsl_extension.register_module_importer+ with a loader function, as
-follows:
+to be imported.
+To define such an external module loader, a plug-in shall call the
+\verb+Acsl_extension.register_module_importer+ with a suitable loader function.
+The loader function is responsible for resolving the module name and defining
+the associated \acsl logic types, functions and predicates. Here is an example
+of such a loader function:
\begin{lstlisting}[language=OCaml]
open Cil_types
@@ -4169,10 +4180,34 @@ invoked multiple times by the kernel, e.g. when a given module is imported from
different source files. Although the loader itself can use memoization
techniques to save time, the module builder shall be populated on every call.
-For debugging module importers, you can use
-\verb+-kernel-msg-key printer:imported-modules+ together with \verb+-print+.
-Using this message key, the imported modules are printed instead of the
-original \verb+import+ clause.
+When printing the internal AST from \framac command line using \verb+-print+
+option, externally imported modules are listed with one single clause for each,
+with no aliasing in order to avoid any ambiguity. For instance:
+\begin{lstlisting}
+//@ import MyLoader: foo::bar::Jazz \as _ ;
+\end{lstlisting}
+
+Alternatively, you can debug the logical definitions actually imported by any
+driver by using \verb+-print+ with the \verb+printer:imported-modules+ debugging
+key:
+\begin{lstlisting}
+> frama-c ... -print -kernel-message-key printer:imported-modules
+\end{lstlisting}
+
+With this option, the contents of the imported modules are printed like regular
+module definitions, with only a comment to mention the origin of the plug-in:
+\begin{lstlisting}
+/*@ // import MyLoader:
+ module foo::bar::Jazz {
+ ...
+ }
+ */
+\end{lstlisting}
+
+Notice that, when using the \verb+printer:imported-modules+ message key, the
+resulting file will still compile and type-check, but the plug-in extension will
+no more be aware of the external nature of those modules, and it will probably
+\emph{not} work as with the original specification.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index acdc7abe54..08b566ed76 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -35,51 +35,9 @@ It is in particular used by the WP plug-in (see \cite{wp} for more information).
\section{External Module Importers}
-Plug-ins have the possibility to load \acsl module from external sources.
-A typical usage is to import \acsl logical declarations from other
-languages, eg. \textsf{Coq} or \textsf{Why3}.
-
-External \acsl module importation is triggered by special \verb+import+ global
-annotations:
-\begin{lstlisting}
-//@ import <loader>: <module-name> [ \as <alias-name> ];
-\end{lstlisting}
-The syntax is similar to the geneal \verb+import+ annotation, except that the
-module name is prefixed with the name of the loader extension. Loader names are
-defined by plugin extensions and you shall refer to the documentation of your
-plug-ins to know the loaders they provides.
-
-The same external module can be imported several times under any aliases, in
-which case they all refer to the same logical specifications, like regular
-modules.
-
-When printing the internal AST from \FramaC command line using \verb+-print+
-option, externally imported modules are listed with one single clause for each,
-with no aliasing in order to avoid any ambiguity. For instance:
-\begin{lstlisting}
-//@ import MyLoader: foo::bar::Jazz \as _ ;
-\end{lstlisting}
-
-Alternatively, you can debug the logical definitions actually imported by any
-driver by using \verb+-print+ with the \verb+printer:imported-modules+ debugging
-key:
-\begin{lstlisting}
-> frama-c ... -print -kernel-message-key printer:imported-modules
-\end{lstlisting}
-
-With this option, the contents of the imported modules are printed like regular
-module definitions, with only a comment to mention the origin of the plug-in:
-\begin{lstlisting}
-/*@ // import MyLoader:
- module foo::bar::Jazz {
- ...
- }
- */
-\end{lstlisting}
-Notice that, when using the \verb+printer:imported-modules+ message key, the
-resulting file will still compile and type-check, but the plug-in extension will
-no more be aware of the external nature of those modules, and it will probably
-\emph{not} work as with the original specification.
+{\color{red}\paragraph{TODO.}
+There is currently no external module importer defined in the platform.
+}
%%% Local Variables:
%%% mode: latex
--
GitLab