From 5c735edcfc1fbafc11b0ea75277ff025ef62bd3e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 24 Jun 2024 10:33:16 +0200
Subject: [PATCH] [userman] documenting external module extensions
---
doc/userman/user-acsl.tex | 50 ++++++++++++++++++++++++++++++++++++++-
1 file changed, 49 insertions(+), 1 deletion(-)
diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 9da27d2c8d4..acdc7abe548 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -14,7 +14,7 @@ extensions coming from an unloaded plug-in can be ignored this way. For
example, if \Eva is not loaded, \lstinline|\eva::unroll _| annotations will be
ignored with a warning, whereas \lstinline|unroll _| cannot be identified as
being supported by Eva, which means that it can only be treated as a user
-error.
+error.
\section{Handling indirect calls with \texttt{calls}}
\label{acsl:calls}
@@ -33,6 +33,54 @@ indicates that the pointer \lstinline|f| can point to any one of
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.
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "userman"
--
GitLab