diff --git a/doc/userman/description.tex b/doc/userman/description.tex
index 3e68c71cc69bfe0b7f48c122d9faef0422e47c1f..687a7c0d113e6ba54339fa6f098a87793cc3fe4e 100644
--- a/doc/userman/description.tex
+++ b/doc/userman/description.tex
@@ -193,7 +193,7 @@ Warning messages from \irg can be controlled with the \lstinline|-warn| option o
In normal use within \framac, the \irg executable is
invoked automatically. However, it can also be run standalone.
In this mode it accepts command-line options and a single input file;
-it produces a C AST representing the translated \cpp, in the Cil (C Intermediate language) text format.
+it produces a C AST representing the translated \cpp, in a text formati similar to Cabs.
The exit code from \irg (and the \fclang plug-in) is
\begin{itemize}
@@ -209,6 +209,9 @@ The exit code from \irg (and the \fclang plug-in) is
These options that are specific to \irg and must be specified by using \option{-cpp-extra-args}:
\begin{itemize}
+ \item \option{-h} -- print help information
+ \item \option{-help} -- print more help information
+ \item \option{-{-}version} -- print version information
\item \option{-o <file>} -- specifies the name and location of the output file (that is, the file to contain the generated AST). The output path may be absolute or relative to the current working directory. \textit{This option is required.}
\item \option{-{-}info=<n>} -- sets the level of informational messages to \textbf{n}; 0 is completely quiet; increasing values are
more verbose. \\
@@ -252,7 +255,6 @@ You can see a list of options by running
The most significant \cl options are these:
\begin{itemize}
\item \option{-I <dir>} -- adds a directory to the include file search path. Using absolute paths is recommended; relative paths are relative to the current working directory.
- \item \option{-{-}version} -- print version information
\end{itemize}
Although \clang can process languages other than \cpp, \cpp is the only one usable with \fclang.
diff --git a/doc/userman/limitations.tex b/doc/userman/limitations.tex
index 588716fb1302c3c9c5c7ae294ec6114ab89d682e..b19b634fe3e5d77d32e7ac80921f9890d335c228 100644
--- a/doc/userman/limitations.tex
+++ b/doc/userman/limitations.tex
@@ -27,13 +27,22 @@ These \acslpp features are not yet implemented
\item set comprehensions
\item using (namespace) declarations (parsed but has no effect)
\item pure functions (parsed but incompletely implemented)
-\item throws clause (parsed but not implemented in Frama-C)
+\item throws clause (parsed but not implemented in \framac)
\item interaction of throws and noexcept
\item parallel \textbackslash let
-\item frama-clang info/warn/error messages are not yet properly categorized and integrated with -fclang-log, -fclang-msg-key, fclang-warn-key. In particular, clang messages are completely independent
+\item frama-clang info/warn/error messages are not yet properly categorized and integrated with -fclang-log, -fclang-msg-key, fclang-warn-key. In particular, clang messages are completely independent of the \framac logging framework
\item \textbackslash count and \textbackslash data are parsed but not yet implemented in \framac
\item semantics of multiple inheritance for annotations
\item formal parameters that are references have pre and post states
+\item dynamic casting not yet implemented in \framac
+\item rounding mode; additional builtin functions
+\item builtin types list and \textbackslash set and related builtin functions
+\item \textbackslash valid\_function \textbackslash allocable \textbackslash freeable \textbackslash fresh are not yet implemented by \framac
+\item extended quantifiers are not yet implemented by \framac
+\item global invariants are not yet implemented by \framac
+\item generalized invariant is not yet implemented by \framac
+\item assigns with both \textbackslash from and = is not yet implemented
+\item ghost code is not yet implemented
\end{itemize}
@@ -42,7 +51,7 @@ These \acslpp features are not yet implemented
\begin{itemize}
\item parsing routines need work to improve robustness, to improve accuracy of locations, and to guard against leaking memory when parses fail
\item the term/predicate parsing methods should be refactored to avoid deep call stacks
-
+\item resolve question of lookup priority between C variables and logic constants (issue \#690)
\end{itemize}
%% Types for ternary, +/-, * etc. , unary & and *
@@ -54,4 +63,4 @@ These \acslpp features are not yet implemented
%% Refactor backtracking to reuse clang tokens instead of ACSL tokens
-at 4100
\ No newline at end of file
+at 4100
diff --git a/doc/userman/macros.tex b/doc/userman/macros.tex
index 654de0cebfe611f5be088a7dd086ea71772f19a1..a0bcc8512655750dc99d56542550dab93fd52132 100644
--- a/doc/userman/macros.tex
+++ b/doc/userman/macros.tex
@@ -53,7 +53,7 @@
\newcommand{\changeinsection}[2]{\textbf{Section \ref{sec:#1}:} #2.}
\newcommand{\todo}[1]{{\large \textbf{TODO: #1.}}}
-\newcommand{\option}[1]{\texttt{#1}}
+\newcommand{\option}[1]{\lstinline|#1|}
\newcommand{\markdiff}[1]{{\color{blue}{#1}}}
\newenvironment{markdiffenv}[1][]{%
diff --git a/doc/userman/main.tex b/doc/userman/main.tex
index 214a3df64c976912590e5302d83e7750261067e9..b4d73269cbf507408be47e45d9a469cc5390986c 100644
--- a/doc/userman/main.tex
+++ b/doc/userman/main.tex
@@ -98,6 +98,8 @@ No. 731453.
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
@@ -114,8 +116,6 @@ These items are not yet addressed
\item \lstinline|__FC_MACHDEP| vs. the option
\item fix where version option is described
\item Need to test that the various kinds of static\_cast actually work as expected.
-\item dynamic casting not yet working
-\item rounding mode; additional builtin functions
\end{itemize}
Bugs
diff --git a/doc/userman/preprocessing.tex b/doc/userman/preprocessing.tex
index 421c930d0cfea7270f230b83f1da65765b7c665f..c89638938b8c4bad8f5049594bec01548360f066 100644
--- a/doc/userman/preprocessing.tex
+++ b/doc/userman/preprocessing.tex
@@ -107,7 +107,7 @@ Accordingly, \acslpp imposes constraints on the directives that may be present w
\item \texttt{if}, \texttt{ifdef}, \texttt{ifndef}, \texttt{elif}, \texttt{else}, \texttt{endif} are permitted but must be completely nested within the annotation in which they appear (an \texttt{endif} and its corresponding \texttt{if}, \texttt{ifdef}, \texttt{ifndef}, or \texttt{elif} must both be in the same annotation comment.)
\item \texttt{warning} and \texttt{error} are permitted
\item \texttt{include} is permitted, but will cause errors if it contains, as is almost always the case, other disallowed directives
- \item \texttt{line} - is not permitted
+ \item \texttt{line} is not permitted
\item \texttt{pragma} and the \texttt{\_Pragma} operator are not permitted
\item stringizing (\verb|#|) and string concatenation (\verb|##|) operators are permitted
\item the \verb|defined| operator is permitted