Edits prior to review

doc/userman/description.tex

@@ -41,6 +41,31 @@ make install
 \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|.
 
+%\section{Current status}
+%
+%Currently on Ubuntu 17.10 and MacOSX (Sierra 10.12.6), \fclang builds in this configuration:
+%
+%\begin{itemize}
+%\item Install opam (>= 2.0)
+%\item disable sandboxing by commenting out the last six lines of ~/.opam/config
+%\item Install ocaml (\lstinline|opam install ocaml|)
+%\item Install bwrap (\lstinline|opam install bwrap|)
+%\item Install menhir, ocamlfind, camlp4, why3, alt-ergo, frama-c
+%\end{itemize}
+%
+%To build against current development:
+%
+%
+%To build against the released Potassium build:
+%
+%
+%
+%\begin{itemize}
+%\item \fclang branch \lstinline|cok-new-parser|, framac commit \lstinline|stable/potassium|,why3 version 0.88.3, alt-ergo version 2.0.0, llvm/clang 6.0, ocaml version 4.05.0
+%
+%\item \fclang branch \lstinline|cok-new-parser|, \framac branch master (commit 83b5e367ff), with why3 version 1.0
+%\end{itemize}
+
 \chapter{Running the plug-in}
 
 \section{\cpp files}
@@ -53,7 +78,7 @@ reinstalling the plugin.
 \section{Frama-clang executable}
 The plug-in operates by invoking the executable \irg (which must be on the system \verb|$PATH|)
 on each file identified as \cpp, in turn. 
-For each file it produces a temporary output file containing the \C AST, which is then itranslated and passed on as input to \framac. 
+For each file it produces a temporary output file containing an equivalent \C AST, which is then translated and passed on as input to \framac. 
 This executable is a single-file-at-a-time command-line executable only. 
 Various options control its behavior.
 
@@ -86,7 +111,7 @@ shows all \fcl-specific options.
 
 The most important of the options are these:
 \begin{itemize}
-\item \option{-help} -- introduction to \framac help
+\item \option{--help}  or \option{-h} -- introduction to \framac help
     \item \option{-kernel-h}, \option{-fclang-h} -- help information about \fc, the \fc kernel and the \fcl plug-in
 	\item \option{-cpp-extra-args <string>} -- the single string argument to this option is \textit{prepended} to the command-line when 
 	\lstinline|frama-clang| is invoked internally. It is particularly 
@@ -97,9 +122,12 @@ The most important of the options are these:
     \item \option{-print} -- prints out the input file seen by \fc; when \fcl is being used this is the input file after pre-processing and translation from \cpp to \C. Thus this output can be useful to see (and debug) the results of \fcl's transformations.
     \item \option{-kernel-warn-key=annot-error=<val>} sets the behavior of \framac, including \fclang, when a parsing error is encountered. The default value (set by the kernel) is \texttt{abort}, which terminates processing upon the first error; a more useful alternative is \texttt{active}, which reports errors but continues processing further annotations.
 	\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{-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| and \lstinline|-kernel-msg-key help| for lists of wawrning categories
+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-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)
@@ -121,7 +149,7 @@ The \fcl option only affects the \fcl plugin, whereas
 The system header files supplied by \fcl may 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{\lstinline|frama-c -cpp-extra-args="-Iinc"{ }-wp a.cpp|}
+\centerline{\texttt{frama-c -cpp-extra-args="-Iinc" -wp a.cpp}}
 
 \section{32 and 64-bit targets}
 \label{sec:bit}
@@ -134,7 +162,7 @@ Consequently, \framac has some options that allow the user to state what machine
 \item The \option{-machdep} option to \framac. See the allowed values using the command\\
 \centerline{ \lstinline|frama-c -machdep help|.}
  For example, with a value of \lstinline|x86_32|, \lstinline|sizeof(long)| has a value of 4, whereas with the option \option{-machdep x86\_64}, \lstinline|sizeof(long)| has a value of 8.
-\item Alternately, the value of \option{-machdep} can be set instead using an environment variable: \lstinline|__FC_MACHDEP|. The variable can be set either in the shell environment or on the command line with \lstinline|-D__FC_MACHDEP=...|
+%%\item Alternately, the value of \option{-machdep} can be set instead using an environment variable: \lstinline|__FC_MACHDEP|. The variable can be set either in the shell environment or on the command line with \lstinline|-D__FC_MACHDEP=...|
 
 \end{itemize}
 
@@ -144,7 +172,7 @@ Consequently, \framac has some options that allow the user to state what machine
 Output messages arise from multiple places: from the \fcl plugin, from the \irg lexer and parser, from the \clang parser, and from the \framac kernel (as well as from any other plugins that may be invoked, such as the \texttt{wp} plug-in). 
 They are controlled by a number of options within the \framac kernel and each plugin. Remember that \cl and \irg options must be put in the \lstinline|-cpp-extra-args| option.
 
-Output messages, including errors, are written to standard out, not to standard error, with the exception of a few fatal errors that cause immediate termination, such as the inability to launch \irg. These fatal errors are typically caused by misconfiguration of the installation.
+Output messages, including errors, are written to standard out, not to standard error. 
 
 \subsection{Errors}
 
@@ -152,8 +180,7 @@ Error messages are always output.
 The key question is whether processing stops or continues upon encountering an error. 
 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|-Werror| is a clang and \irg option that causes any parser warnings to be treated as errors
-\item \lstinline|--stop-annot-error| is a \irg option that causes prompt termination on errors (the \irg default is to continue)
+\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}.
 \end{itemize}
 
@@ -165,6 +192,8 @@ 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.
 
 \begin{itemize}
+\item \lstinline|-Werror| is a clang and \irg option that causes any parser warnings to be treated as errors
+\item \lstinline|-w| is a clang and \irg option that causes any parser warnings to be ignored
 \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|
@@ -191,22 +220,27 @@ it produces a C AST representing the translated \cpp, in a text format similar t
 The exit code from \irg is
 \begin{itemize}
 \item 0 if processing is successful, including if only warnings or informational messages are emitted
-\item 0 if there are non-fatal errors but \option{--no-exit-code} is enabled (the default)
-\item 1 if there are non-fatal errors but \option{--exit-code} is enabled
+\item 0 if there are some non-fatal errors but \option{--no-exit-code} is enabled (the default)
+\item 1 if there are some non-fatal errors but \option{--exit-code} is enabled, or if there are warnings and \lstinline|-Werror| is enabled, but \lstinline|-w| is not.
 \item 2 if there are fatal errors
 \end{itemize}
+Fatal errors are those resulting from misconfiguration of the system; non-fatal errors are the result of errors in the user input (e.g. parsing errors).
+
+The \option{-Werror} option causes warnings to be treated as errors. 
 
-The \option{-Werror} \irg option causes warnings to be treated as errors.
+All output is sent to the standard output.\footnote{Currently clang output goes to std err.}
 
 \section{\irg specific options}
 \label{sec:fcloptions}
 
-These options that are specific to \irg.
+These options are specific to \irg.
 \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{-w} -- suppress warnings (overrides \option{-Werror})
+	\item \option{-Werror} -- treat warnings as errors 
 	\item \option{-{-}info=<n>} -- sets the level of informational messages to \textbf{n}; 0 is completely quiet; increasing values are
 	more verbose. \\
 	\option{-{-}info} sets the level to 1 \\
@@ -250,6 +284,8 @@ 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{-w} -- suppress clang warnings
+	\item \option{-Werror} -- treat warnings as errors
 \end{itemize}
 
 Although \clang can process languages other than \cpp, \cpp is the only one usable with \fclang.

doc/userman/fclangversion.tex

 \newcommand{\version}{0.1-REVIEW\xspace}
 \newcommand{\fclangversion}{0.1.0-REVIEW\xspace}
-\newcommand{\fcversion}{Potassium+\xspace}
+\newcommand{\fcversion}{Potassium\xspace}
 \newcommand{\clangversion}{6.0-8.0\xspace}

doc/userman/grammar.tex

@@ -13,7 +13,7 @@ Consequently during the VESSEDIA project, the scanner and parser were completely
 The new parser uses a recursive descent design in which the names of functions doing the parsing can match the names of non-terminals in the grammar. 
 Consequently the implementation of the parser is much more readable, human checkable, and modifiable as the \acslpp language evolves. 
 The drawback of this design is that \acslpp is not LL(1); it is not even LL(k) for fixed k. 
-Thus some amount of backtracking is required. 
+Thus some amount of lookahead and backtracking is required. 
 The bulleted paragraphs below describe the problematic aspects of \acslpp and how they are addressed.
 
 The principal goal of an LL(k) formulation of a grammar is to be able to predict which grammar production is being seen in the input stream from a small amount of look-ahead.

doc/userman/limitations.tex

@@ -14,6 +14,7 @@ The following C++ features are not implemented in \acslpp.
 \item preprocessing is restricted within \acslpp annotations (cf. \S\ref{sec:preprocessing})
 \item uses of typename
 \item uses of templates are not robust
+\item uses of typeid
 \end{itemize}
 
 \section{Implementation of \acslpp}
@@ -32,7 +33,6 @@ These \acslpp features are not yet implemented
 \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 of the \framac logging framework
 \item \textbackslash count and \textbackslash data are parsed but not yet implemented in \framac
 \item formal parameters that are references have pre and post states
 \item dynamic casting not yet implemented in \framac
@@ -43,16 +43,17 @@ These \acslpp features are not yet implemented
 \item global invariants are not yet implemented by \framac
 \item generalized invariants are not yet implemented by \framac
 \item assigns with both \textbackslash from and = is not yet implemented
-\item \option{-fclang-version} is not implemented
 \end{itemize}
 
 \section{\acslpp implementation}
 
 \begin{itemize}
+\item \option{-fclang-version} is not implemented
 \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 issues of tset representations
 \item cannot change the set of C++ suffixes
+\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
 \end{itemize}
 
 %% Types for ternary, +/-, * etc. , unary & and *

doc/userman/main.tex

@@ -59,7 +59,8 @@ CEA LIST\\ Software Reliability \& Security Laboratory
 \addcontentsline{toc}{chapter}{Foreword}
 
 This is the user manual for the \framac plug-in
-\fclang\footnote{\url{https://frama-c.com/frama-clang.html}}. The contents of this
+\fclang.\footnote{\url{https://frama-c.com/frama-clang.html}} 
+The contents of this
 document correspond to version \fclangversion of the plug-in compatible with the
 \fcversion version of \framac~\cite{userman,fac15}.  The development of
 the \fclang plug-in is still ongoing.  Features described by this document will certainly
@@ -108,12 +109,9 @@ These items are not yet addressed
 \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 Review the preprocessor tokens
 \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 check behavior of -stop-annot-error
-\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.
 \end{itemize}
@@ -128,6 +126,8 @@ Bugs
 \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}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

doc/userman/preprocessing.tex

@@ -39,27 +39,23 @@ punctuation character sequences. Digraphs in \acslpp annotations are translated
 Using digraphs is not recommended.
 
 \section{Preprocessor tokens}
-Preprocessor tokens (per CPP) belong to one of five categories. White space (space, tab) serves only to separate tokens; it is not needed between tokens whose concatenation is not a single token. Line terminators also separate tokens and also delineate certain features: preprocessing directives and string literals do not extend over more than one (logical) line.
-\begin{itemize}
-	\item identifiers: character sequences that match the regular expression \\
-\centerline{\texttt{[a-zA-Z\_][a-zA-Z\_0-9]*}} \\ 
+Preprocessor tokens (per CPP) belong to one of several categories: identifiers, literals (including numeric, character and string literals), header names,
+operators, punctuation, and single other characters.
+White space (space, tab) serves only to separate tokens; it is not needed between tokens whose concatenation is not a single token. Line terminators also separate tokens and also delineate certain features: preprocessing directives and string literals do not extend over more than one (logical) line.
+
 Dollar signs are also allowed as non-digit identifier characters if the clang option\\ \texttt{-fdollars-in-identifiers} is enabled, which it is by default. \\
 Enable with \texttt{-fdollars-in-identifiers} ; \\disable with \texttt{-fno-dollars-in-identifiers} .
-	\item number: character sequences that match the regular expression  \\
-\centerline{\texttt{[.]?[0-9]([0-9a-zA-Z.]|[eEpP][+-]))*}}  \\
 
-	\item string literals: character sequence enclosed in " " or ' ' or < >, with \lstinline|\"| for \lstinline|"| in a double-quoted literal (that is not a header file name) and \lstinline|\'| for \lstinline|'| in a single-quoted literal, and \lstinline|\\| for \lstinline|\| in either. After all other preprocessor phases are complete, the preprocessor concatenates adjacent string literals.
-	\item punctuator: all single non-alphanumeric printable characters except 
-\verb|@|, \verb|#| and \verb|`|, and all multi-punctuation sequences that meaningful to \C/\cpp (e.g. > and >{>}= ), but not an arbitrary multi-punctuation character sequence.
-	\item other tokens: \verb|@|, \verb|#|, \verb|`| and all non-ASCII single characters.
-\end{itemize}
-The above token definitions imply that arbitrary text can always be broken into
-legitimate preprocessor tokens, with the exception of a few characters and of badly formed unicode sequences.
+Numeric literals are more general than a C++ or \acsl number. 
+Nevertheless, aside from token concatenation, each preprocessing token
+becomes a compiler token, which then may be an illegal compiler token.
 
+The token definitions imply that arbitrary text can always be broken into
+legitimate preprocessor tokens, with the exception of a few characters and of badly formed unicode sequences.
 
 Note that not all preprocessor tokens are valid \C/\cpp parser tokens. Tokens in the other category have no meaning to \C/\cpp and the \texttt{number} category allows many sequences that are not legal \C/\cpp numeric tokens. These tokens will generally provoke compiler errors. For example in \C/\cpp, 0..2 is one token and is not interpreted as two consecutive numeric tokens.
 
-\acsl and \acslpp have slightly different tokens than the above, so the preprocessor tokens need to be re-tokenized in some cases:
+\acsl and \acslpp have slightly different tokens than the preprocessor, so the preprocessor tokens need to be re-tokenized in some cases:
 \begin{itemize}
 	\item The \verb|@| token is a whitespace character in the interior of a \acslb annotation.
 	\item There are some \acslb multi-character punctuator tokens that are not