diff --git a/doc/userman/description.tex b/doc/userman/description.tex
index 7463eca4f74935029c1092b19f5152e8eb71ada6..d2cee997f8e76e5cfd3d26e6e4cf37d836d6d277 100644
--- a/doc/userman/description.tex
+++ b/doc/userman/description.tex
@@ -32,14 +32,17 @@ with \acslpp annotations giving their specifications.
The plugin can be built by hand from source using the following commands. Create a new directory to which you download and unpack the source distribution. Then \lstinline|cd| into the source directory itself (one level down) and execute:
\begin{listing-nonumber}
-make distclean
-autoconf -f
-./configure --prefix=<opamroot>
+./configure
make
make install
\end{listing-nonumber}
-\lstinline|<opamroot>| should be the absolute path of the root of the opam installation, e.g., something like \lstinline|~/.opam/4.05.0| or \lstinline|~/.opam/system|. If \framac has been installed independently of \lstinline|opam|, then set \lstinline|<opamroot>| above so that the location of the \framac executable (that is, the result of executing \lstinline|which frama-c|) is
-\lstinline|<opamroot>/bin/frama-c|.
+
+By default, \fclang will install its files under the same root
+directory as \framac itself. In particular, if \framac has been
+installed from \lstinline|opam|, the installation will be done under
+\verb|$(opam var prefix)| directory. Standard configure options for
+manipulating installation directories are available, notably
+\verb|--prefix|.
%\section{Current status}
%
@@ -124,10 +127,10 @@ The most important of the options are these:
\item \option{-machdep <arg>} -- sets the target machine architecture, cf. \S\ref{sec:bit}
\item \option{-kernel-msg-key <categories>} -- sets the amount of informational messages according to different categories of messages.
See \lstinline|-kernel-msg-key help| for a list of informational categories.
- \item \option{-kernel-warn-key <categories>} -- sets the amount and behavior of warnings.\\ See \lstinline|-kernel-msg-key help| for a list of warning categories.
+ \item \option{-kernel-warn-key <categories>} -- sets the amount and behavior of warnings.\\ See \lstinline|-kernel-warn-key help| for a list of warning categories.
\item \option{-fclang-msg-key <categories>} -- sets the amount of informational messages according to different categories of messages.
See \lstinline|-fclang-msg-key help| for a list of informational categories.
- \item \option{-fclang-warn-key <categories>} -- sets the amount and behavior of warnings.\\ See \lstinline|-fclang-msg-key help| for a list of warning categories.
+ \item \option{-fclang-warn-key <categories>} -- sets the amount and behavior of warnings.\\ See \lstinline|-fclang-warn-key help| for a list of warning categories.
\item \option{-fclang-verbose <n>} -- sets the amount of information from the \fclang plug-in
\item \option{-fclang-debug <n>} -- sets the amount of debug information from the \fclang plug-in
\item \option{-annot} -- enables processing \acslpp annotations (enabled by default)
@@ -137,7 +140,9 @@ See \lstinline|-fclang-msg-key help| for a list of informational categories.
Note that the \framac option \verb|-no-pp-annot| is ignored by \fclang. Preprocessing is always performed on the source input (unless annotations are ignored entirely using \verb|-no-annot|).
\section{Include directories}
-By default \irg is given the paths to the two directories containing the \fcl and \fc header files, which include \acslpp specifications for the \cpp library functions. The default paths to these directories are set by the \lstinline|-cxx-c++stdlib-path| and\\
+By default \irg is given the paths to the two directories containing the \fcl and \fc header files, which include \acslpp specifications for the \cpp library functions. The default paths (\verb|$FRAMAC_SHARE/libc++| and
+\verb|$FRAMAC_SHARE/libc| respectively) to these directories
+can be overriden by the \fcl options \lstinline|-cxx-c++stdlib-path| and\\
\lstinline|-cxx-cstdlib-path| options.
Users typically have additional header files for their own projects. These are supplied to the \fcl preprocessor using the option \lstinline|-cpp-extra-args|.
@@ -146,7 +151,7 @@ You can use \lstinline|-fclang-cpp-extra-args| instead of \lstinline|cpp-extra-a
The \fcl option only affects the \fcl plugin, whereas
\lstinline|-cpp-extra-args| may be seen by other plugins as well, if such plugins do their own preprocessing. Also note that the presence of any instance of \lstinline|-fclang-cpp-extra-args| will cause uses of \lstinline|-cpp-extra-args| to be ignored.
-The system header files supplied by \fcl may not include all \cpp system files. Omissions should be reported to the \fc team.
+The system header files supplied by \fcl does not include all \cpp system files. Omissions should be reported to the \fc team.
As an example, to perform \lstinline|wp| checking of files \lstinline|a.cpp| and \lstinline|inc/a.h|, one might use the command-line \\
\centerline{\texttt{frama-c -cpp-extra-args="-Iinc" -wp a.cpp}}
@@ -181,15 +186,17 @@ The key question is whether processing stops or continues upon encountering an e
Continuing can result in a cascade of unhelpful error messages, but stopping immediately can hide errors that occur later in source files.
\begin{itemize}
\item \lstinline|--stop-annot-error| is a \irg option that causes prompt termination on annotations errors (the \irg default is to continue); this does not respond to errors in C++ code
-\item \lstinline|-fclang-warn-key=annot-error=abort| is a \fcl plug-in option that will invoke \irg with \lstinline|--stop-annot-error|. \lstinline|error| and \lstinline|error_once| (instead of \lstinline|abort|) have the same effect; other values for the key will allow continuing after errors. The default is \texttt{abort}.
+\item \lstinline|-kernel-warn-key=annot-error=abort| is a \fcl plug-in option that will invoke \irg with \lstinline|--stop-annot-error|. \lstinline|error| and \lstinline|error_once| (instead of \lstinline|abort|) have the same effect; other values for the key will allow continuing after errors. The default is \texttt{abort}.
\end{itemize}
\subsection{Warnings}
-The various categories of warnings from \fcl can be seen with the command \\ \centerline{\lstinline|frama-c -fclang-warn-key help|}
-Warning messages are emitted by default.
+%The various categories of warnings from \fcl can be seen with the command \\ \centerline{\lstinline|frama-c -fclang-warn-key help|}
+%Warning messages are emitted by default.
-Warning messages from \irg can be controlled with the \lstinline|-warn| option of \irg, or, equivalently, the \lstinline|-fclang-warn-key=parse| option of \fc.
+Warning messages from \irg can be controlled with the \lstinline|-warn| option of \irg.
+% Note in the current version
+%, or, equivalently, the \lstinline|-fclang-warn-key=parse| option of \fc.
\begin{itemize}
\item \lstinline|-Werror| is a clang and \irg option that causes any parser warnings to be treated as errors
@@ -197,8 +204,9 @@ Warning messages from \irg can be controlled with the \lstinline|-warn| option o
\item the \irg option \lstinline|--no-warn| or \lstinline|--warn=0| turns off \irg warning messages
\item the \irg option \lstinline|--warn=<n>|, with $n > 0$ turns on \irg warning messages; the higher the value $n$ the more messages
\item the \irg option \lstinline|--warn| is the same as \lstinline|--warn=1|
-\item the \fc option \lstinline|-fclang-warn-key=parse=inactive| is the same as the \irg option \lstinline|--warn=0|
-\item the \fc option \lstinline|-fclang-warn-key=parse=active| is the same as the \irg option \lstinline|--warn=1|
+% Cf above.
+%\item the \fc option \lstinline|-fclang-warn-key=parse=inactive| is the same as the \irg option \lstinline|--warn=0|
+%\item the \fc option \lstinline|-fclang-warn-key=parse=active| is the same as the \irg option \lstinline|--warn=1|
\end{itemize}
\textit{The \clang options are not currently integrated with the \fc warning and error key system.}
diff --git a/doc/userman/introduction.tex b/doc/userman/introduction.tex
index 6f780bd51587476c3216c54ad649680d6f8b6bff..153ccad068151e00262bae8359f32567131f8dc3 100644
--- a/doc/userman/introduction.tex
+++ b/doc/userman/introduction.tex
@@ -19,7 +19,3 @@ The following sections describe the current status and limitations of the curren
(cf. \url{https://clang.llvm.prg/cxx_status.html}).
However, \fclang may not support all of the features of \cpp within annotations.
\end{itemize}
-
-The source material for this document is in Frama-C's gitlab repository:\\ \centerline{\url{git@git.frama-c.com:frama-c/frama-clang.git},} \\
- in directory \lstinline|doc/userman| (in branch \lstinline|cok-doc|).
-
diff --git a/doc/userman/limitations.tex b/doc/userman/limitations.tex
index 1476d89a096854abb45c3d6ad57a3527834d2072..ed2dc33a14993d01783727c008095cd59ddda930 100644
--- a/doc/userman/limitations.tex
+++ b/doc/userman/limitations.tex
@@ -45,7 +45,7 @@ These \acslpp features are not yet implemented
\item assigns with both \textbackslash from and = is not yet implemented
\end{itemize}
-\section{\acslpp implementation}
+\section{Other \fcl limitations}
\begin{itemize}
\item \option{-fclang-version} is not implemented
diff --git a/doc/userman/main.tex b/doc/userman/main.tex
index df52cdc80744893ba40e5af5641cee4824eb2972..2a6adce6da132eafe9234810239ad3597a075ba6 100644
--- a/doc/userman/main.tex
+++ b/doc/userman/main.tex
@@ -69,7 +69,7 @@ evolve in the future.
\section*{Acknowledgements}
We gratefully thank the people who contributed to this document:
-David R. Cok, Virgile Prevosto, Armand Puccetti, Franck Verdrine.
+David R. Cok, Virgile Prevosto, Armand Puccetti, Franck Védrine.
This document was written in the context of project VESSEDIA,
which received funding from the European Union's 2020
@@ -94,41 +94,41 @@ No. 731453.
\include{changes}
-\section*{TODO}
-
-These items are not yet addressed
-\begin{itemize}
-\item Add/revise list of contributors/reviewers
-\item permanent location of source documents
-\item generation of doxygen
-\item (Introduction) Verify the version of \framac and \clang supported
-\item Sort out the interactions among the options -verbose -debug -quiet -fclang-debug -fclang-verbose -fclang-msg-key -fclang-warn-key
-\item -no-pp-annot is not recognized by \fclang
-\item Add comments about using system header files
-\item Comment on the demangling options
-\item Review the clang and \irg options
-\item describe the framaCIRGen options: -x -b -v --gen-impl-meth
-\item Comment on handling of unicode in the preprocessor
-\item must the argument of -cpp-extra-args always be given with an = and quoted string
-\item Interactions between \_\_FC\_MACHDEP and -machdep
-\item Check whether static or dynamic linking is used in building
-\item fix where version option is described
-\item Need to test that the various kinds of static\_cast actually work as expected.
-\end{itemize}
-
-Bugs
-\begin{itemize}
-\item Various parts of the tool use stdout and stderr differently
-\item non-clang options not included in framaCIRGen -help
-\item The -o option is required
-\item Fix how to do custom ASTs; The custom build instructions with a prefix to a temp directory fail
-\item it appears that trigraph processing cannot be turned off, is on by default for \irg but off by default for clang++; not sure why
-\item it does not seem that clang options are passed through, e.g. -fdollars-in-identifiers; \irg defaults are different than clang
-\item preprocessor implementation does not concatenate string literals
-\item spurious error when running framaCIRGen -help
-\item Clang output goes to std::cerr instead of std::cout
-\item -Werror is not being passed through to clang, though -w is
-\end{itemize}
+% \section*{TODO}
+
+% These items are not yet addressed
+% \begin{itemize}
+% \item Add/revise list of contributors/reviewers
+% \item permanent location of source documents
+% \item generation of doxygen
+% \item (Introduction) Verify the version of \framac and \clang supported
+% \item Sort out the interactions among the options -verbose -debug -quiet -fclang-debug -fclang-verbose -fclang-msg-key -fclang-warn-key
+% \item -no-pp-annot is not recognized by \fclang
+% \item Add comments about using system header files
+% \item Comment on the demangling options
+% \item Review the clang and \irg options
+% \item describe the framaCIRGen options: -x -b -v --gen-impl-meth
+% \item Comment on handling of unicode in the preprocessor
+% \item must the argument of -cpp-extra-args always be given with an = and quoted string
+% \item Interactions between \_\_FC\_MACHDEP and -machdep
+% \item Check whether static or dynamic linking is used in building
+% \item fix where version option is described
+% \item Need to test that the various kinds of static\_cast actually work as expected.
+% \end{itemize}
+
+% Bugs
+% \begin{itemize}
+% \item Various parts of the tool use stdout and stderr differently
+% \item non-clang options not included in framaCIRGen -help
+% \item The -o option is required
+% \item Fix how to do custom ASTs; The custom build instructions with a prefix to a temp directory fail
+% \item it appears that trigraph processing cannot be turned off, is on by default for \irg but off by default for clang++; not sure why
+% \item it does not seem that clang options are passed through, e.g. -fdollars-in-identifiers; \irg defaults are different than clang
+% \item preprocessor implementation does not concatenate string literals
+% \item spurious error when running framaCIRGen -help
+% \item Clang output goes to std::cerr instead of std::cout
+% \item -Werror is not being passed through to clang, though -w is
+% \end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%