doc/userman/fclangversion.tex

-\newcommand{\version}{0.0.9\xspace}
-\newcommand{\fclangversion}{0.0.9\xspace}
-\newcommand{\fcversion}{21.x~Scandium\xspace}
-\newcommand{\clangversion}{6.0-10.0\xspace}
+\newcommand{\fclangversion}{\input{FCLANG_VERSION}\xspace}
+\newcommand{\framacversion}{\input{FC_VERSION}~\input{FC_VERSION_NAME}\xspace}
+\newcommand{\clangversion}{\input{CLANG_VERSION}\xspace}

doc/userman/grammar.tex

-\newcommand{\lang}{C++\xspace}
 \chapter{Grammar and parser for \acslpp}
 \label{sec:grammar}
 
-This section summarizes some of the technical implementation considerations in writing a parser for \acslpp within \fclang. 
-This material may be useful for developers and maintainers of \fclang; it is not needed by users of \fclang.
+This section summarizes some of the technical implementation considerations in writing a parser for \acslpp within \framaclang. 
+This material may be useful for developers and maintainers of \framaclang; it is not needed by users of \framaclang
 
-Recall that \fclang uses clang to parse \lang and a custom parser to parse \acslpp annotations, jointly producing a representation of the \lang and \acslpp source input in the Frama-C intermediate language. 
+Recall that \framaclang uses clang to parse \Cpp and a custom parser to parse \acslpp annotations, jointly producing a representation of the \Cpp and \acslpp source input in the Frama-C intermediate language. 
 The first version of the \acslpp custom parser, written during the STANCE project, used a hand-written bison-like parser, but with function pointers to record state and actions rather than using a tool-generated table to drive the parsing. 
 This design proved to be too brittle and difficult to efficiently evolve as new features were added to \acslpp. 
 Consequently during the VESSEDIA project, the scanner and parser were completely rewritten, largely retaining the previous design's connections to clang, token definitions, name lookup and type resolution, and AST generation.
@@ -18,7 +17,7 @@ The bulleted paragraphs below describe the problematic aspects of \acslpp and ho
 
 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.
 Most \acslpp constructs start with a unique keyword (e.g., clauses begin with \lstinline|requires|, \lstinline|ensures| etc.) which serves this purpopse. 
-But the constructs inherited from \lang pose some challenges.
+But the constructs inherited from \Cpp pose some challenges.
 
 \begin{itemize}
 \item \textbf{Left recursion}. Expression grammars are typically left recursive, which is problematic for recursive descent parsers. 
@@ -41,15 +40,26 @@ Many operations on a data type are also simply element-by-element operations on
 Also, errors found during type-checking can be associated with more readable error messages than those found during parsing.
 
 \item \textbf{cast vs. parenthesized expression} To determine whether an input like \lstinline|(T)-x| is (a) the difference of the parenthesized expression \lstinline|(T)| and \lstinline|x| or (b) a cast of \lstinline|-x| to the type \lstinline|T|, one must know whether \lstinline|T| is a variable or type. 
-This is a classic problem in parsing \lang; it requires that identifiers be known to be either type names or variable names in the scanner. 
+This is a classic problem in parsing \Cpp; it requires that identifiers be known to be either type names or variable names in the scanner. 
 In addition, \lstinline|T| here can be an arbitrary type expression. 
-For example, in \lang, a type expression can contain pointer operators that can look, at least initially like multiplications and they can contain template instantiations that look initially like comparisons. 
-\fclang handles this situation by allowing a backtrackable parse. 
+For example, in \Cpp, a type expression can contain pointer operators that can look, at least initially like multiplications and they can contain template instantiations that look initially like comparisons. 
+\framaclang handles this situation by allowing a backtrackable parse. 
 When a left parenthesis is parsed in an expression context, the parser proceeds by attempting a parse of a cast expression. If the contents of the parenthesis pair is successfully parsed as a type expression, it is assumed to be a cast expression. 
 
 If such a parse fails, no error messages are emitted; rather the parse is rewound and proceeds again assuming the token sequence to be a parenthesized expression.
 
-\item \textbf{set comprehension}. The syntax of the set comprehension expression follows traditional mathematics: \lstinline: { $expr$ | $binders$ ; $predicate$ }:. This structure poses two difficulties for parsers. First, the expression $expr$ may contain bitwise-or operators, so it is not known to the parser whether an occurence of \verb:|: is the beginning of the binders or is just a bitwise-or operator. Second, the expression will use the variables declared in the binders section. However, the binders are not seen until after the expression is scanned. Note that these problems are not unique to a recursive descent design; they would challenge a LR parser just as much. \textit{This particular feature is not yet implemented in \fclang, nor in Frama-C and so is not yet resolved in the parser implementation.}
+\item \textbf{set comprehension}. The syntax of the set comprehension expression
+  follows traditional mathematics:
+  \lstinline:{ $expr$ | $binders$ ; $predicate$}:.
+  This structure poses two difficulties for parsers. First, the expression
+  $expr$ may contain bitwise-or operators, so it is not known to the parser
+  whether an occurence of \verb:|: is the beginning of the binders or is just a
+  bitwise-or operator. Second, the expression will use the variables declared in
+  the binders section. However, the binders are not seen until after the
+  expression is scanned. Note that these problems are not unique to a recursive
+  descent design; they would challenge a LR parser just as much.
+  \textit{This particular feature is not yet implemented in \framaclang,
+    nor in \FramaC and so is not yet resolved in the parser implementation.}
 
 \item \textbf{labeled expressions}. \acslpp allows expressions to have labels, designated by a \lstinline|id : | prefix. 
 So the parser cannot know whether an initial \lstinline|id| is a variable or just a label until the colon is parsed. 
@@ -59,7 +69,7 @@ Ambiguity arises with the use of a colon for the else part of a conditional expr
 So in an expression such as 
 \lstinline| a ? b ? c : d : e : f|, it is ambiguous whether \lstinline|c| or \lstinline|d| or \lstinline|e| is a label. 
 Parenthesizing must be used to solve this problem. 
-\fcl presumes that if the \textit{then} part of a conditional expression is being parsed, a following colon is always the colon introducing the \textit{else} part. That is, the binding to a conditional expression has tighter precedence than to a naming expression.
+\framaclang presumes that if the \textit{then} part of a conditional expression is being parsed, a following colon is always the colon introducing the \textit{else} part. That is, the binding to a conditional expression has tighter precedence than to a naming expression.
 
 \end{itemize}
 

doc/userman/introduction.tex

 \chapter{Introduction}
 
-\framac~\cite{userman,fac15} is a modular analysis framework for the \C
+\FramaC~\cite{userman,baudinCACM21} is a modular analysis framework for the \C
 programming language that supports the \acsl specification
-language~\cite{acsl}. This manual documents the \fclang plug-in of \framac,
+language~\cite{acsl}. This manual documents the \framaclang plug-in of \FramaC,
 version \fclangversion. 
-The \fclang plug-in supports the \acslpp extension of \acsl for \cpp programs and specifications; 
+The \framaclang plug-in supports the \acslpp extension of \acsl for \Cpp programs and specifications; 
 it is built on the \clang\footnote{https://clang.llvm.org/} compiler infrastructure and uses \clang for 
-parsing C++. The plug-in extends \clang to parse \acslpp, translating source files containing \cpp and \acslpp into \framac's intermediate language for \C and \acsl.
+parsing C++. The plug-in extends \clang to parse \acslpp, translating source files containing \Cpp and \acslpp into \FramaC's intermediate language for \C and \acsl.
 
-The \fclang plug-in intends to provide a full translation of \cpp and \acslpp into the \framac internal representation, and from there to allow \cpp programs and \acslpp specifications to be analyzed by other \framac plug-ins. 
+The \framaclang plug-in intends to provide a full translation of \Cpp and \acslpp into the \FramaC internal representation, and from there to allow \Cpp programs and \acslpp specifications to be analyzed by other \FramaC plug-ins. 
 \textit{This is a work in progress.}
 The following sections describe the current status and limitations of the current implementation.
 \begin{itemize}
-	\item The plug-in aims for the C++11 version of \cpp
-	\item \acslpp is described in the companion \acslpp reference manual \cite{acslpp}, also a part of the \framac release.
+	\item The plug-in aims for the C++11 version of \Cpp
+	\item \acslpp is described in the companion \acslpp reference manual \cite{acslpp}, also a part of the \FramaC release.
     \item The plug-in is compatible with version \clangversion of \clang. 
-    This version of \clang supports \cpp versions through C++17 
+    This version of \clang supports \Cpp versions through C++17 
     (cf. \url{https://clang.llvm.prg/cxx_status.html}). 
-    However, \fclang may not support all of the features of \cpp within annotations.
+    However, \framaclang may not support all of the features of \Cpp within annotations.
 \end{itemize}

doc/userman/limitations.tex

 \chapter{Known Limitations}
 
-The development of the \fclang plug-in is still ongoing.
-\fclang does not implement all of current C++ nor all of 
+The development of the \framaclang plug-in is still ongoing.
+\framaclang does not implement all of current \Cpp nor all of 
 \acslpp as defined in its language definition~\cite{acslpp}.
 The most important such limitations are listed in this section.
 
 \textit{These lists are not (nearly) complete}
 
-\section{Implementation of C++}
+\section{Implementation of Cpp}
 
 The following C++ features are not implemented in \acslpp.
 \begin{itemize}
@@ -16,7 +16,7 @@ The following C++ features are not implemented in \acslpp.
 \item uses of templates are not robust
 \item uses of typeid
 \item implementation of the standard library is very rudimentary
-\item main target of \fcl is C++11
+\item main target of \framaclang is C++11
 \end{itemize}
 
 \section{Implementation of \acslpp}
@@ -24,38 +24,38 @@ The following C++ features are not implemented in \acslpp.
 These \acslpp features are not yet implemented
 \begin{itemize}
 
-\item \fclang cannot process annotations that are separate from the source file
-\item \acslpp specifications for standard \cpp library functions are still quite limited
+\item \framaclang cannot process annotations that are separate from the source file
+\item \acslpp specifications for standard \Cpp library functions are still quite limited
 \item \acslpp definitions within template declarations
 \item ghost code is not yet implemented
 \item model declarations
 \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 \framac)
+\item throws clause (parsed but not implemented in \FramaC)
 \item interaction of throws and noexcept
 \item parallel \textbackslash let
-\item \textbackslash count and \textbackslash data are parsed but not yet implemented in \framac
+\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
+\item dynamic casting not yet implemented in \FramaC
 \item rounding mode  and related 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 invariants are not yet implemented by \framac
+\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 invariants are not yet implemented by \FramaC
 \item assigns with both \textbackslash from and = is not yet implemented
 \end{itemize}
 
-\section{Other \fcl limitations}
+\section{Other \framaclang limitations}
 
 \begin{itemize}
-\item \option{-fclang-version} is not implemented
+\item \lstinline|-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
+\item cannot change the set of \Cpp 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 *