From afd9caa387ac0853606aa770d6460dda4eb30813 Mon Sep 17 00:00:00 2001
From: DavidCok <cok@frontiernet.net>
Date: Thu, 25 Jul 2019 16:39:37 +0200
Subject: [PATCH] Edits to the userman
---
doc/userman/description.tex | 28 ++++++++--------------------
doc/userman/fclangversion.tex | 2 +-
doc/userman/introduction.tex | 10 +++++-----
doc/userman/main.tex | 14 +++++++-------
doc/userman/preprocessing.tex | 10 ++++++----
5 files changed, 27 insertions(+), 37 deletions(-)
diff --git a/doc/userman/description.tex b/doc/userman/description.tex
index 6604f0cd..4eb5c1f6 100644
--- a/doc/userman/description.tex
+++ b/doc/userman/description.tex
@@ -1,16 +1,4 @@
-The \fclang plug-in intends to provide a full translation of C++ and \acslpp into the \framac internal representation, and from there be able to be analyzed by other \framac plug-ins. This is a work in progress. The following sections describe the limitations of the current implementation.
-\begin{itemize}
- \item The plug-in aims for the TBD version of C++
- \item \acslpp is described in the companion \acslpp reference manual, also a part of the \framac release.
-\end{itemize}
-
-Notes
-\begin{itemize}
- \item Which version of Clang?
- \item Clang (8) support C++98 (except exported templates, later removed) and C++11 and current draft standard for C++1y
- \item see https://clang.llvm.org/docs/UsersManual.html\#cxx for supported features in clang C++
-\end{itemize}
\chapter{Installation}
@@ -19,10 +7,10 @@ TBD - installation instructions
\chapter{Running the plug-in}
\section{C++ files}
-Once installed the plugin is run automatically by Frama-C on any C++ files listed on the command-line. C++ files are identified by the filename suffix. The default C++ suffixes are these:
+Once installed the plugin is run automatically by Frama-C on any C++ files listed on the command-line. C++ files are identified by their filename suffixes. The default suffixes recognized as C++ are these:
.cpp, .C, .cxx, .ii, .ixx, .ipp, .i++, .inl, .h, .hh
-Currently this set of suffixes is compiled in the plugin (in file frama\_Clang\_register.ml) and can only be changed by recompiling and
+Currently this set of suffixes is compiled in the plugin (in file \texttt{frama\_Clang\_register.ml}) and can only be changed by recompiling and
reinstalling the plugin.
\section{Frama-clang executable}
@@ -38,13 +26,13 @@ option and is \irg by default. The path may be absolute; if it is a relative pat
\section{Frama-clang options}
The options known to the \fcl plugin are processed by the \fc kernel when listed on the \fc command-line.
-The use of the frama-c command-line is described in the core frama-c
+The use of the \fc command-line is described in the core \fc
user guide.
-There are many kernel options that affect all plugins and many options specific to frama-clang.
+There are many kernel options that affect all plugins and many options specific to \fclang.
The command \\
-\lstinline|frama-c -kernel-h| \\
+\centerline{\lstinline|frama-c -kernel-h|} \\
shows all kernel options; the command\\
-\lstinline|frama-c -fclang-h| \\
+\centerline{\lstinline|frama-c -fclang-h|} \\
shows all \fcl-specific options.
The most important of the options are these:
@@ -94,8 +82,8 @@ You can see a list of options by running
The most significant options for \irg are these:
\begin{itemize}
- \item \option{-I} -- adds a directory to the include file search path
- \item \option{-o <file>} -- specifies the location of the output file (in this case, the file to contain the generated AST)
+ \item \option{-I <dir>} -- adds a directory to the include file search path. Using absolute paths is recommended; relative paths are relative to TODO.
+ \item \option{-o <file>} -- specifies the location of the output file (in this case, the file to contain the generated AST). Using absolute paths is recommended; relative paths are relative to TODO.
\item \option{-std=...} -- the input programming language (default is \lstinline|-std=c++11|)
\item \option{-w} -- suppress warnings
\item \option{-{-}version} -- print version information
diff --git a/doc/userman/fclangversion.tex b/doc/userman/fclangversion.tex
index 96766b11..67275e01 100644
--- a/doc/userman/fclangversion.tex
+++ b/doc/userman/fclangversion.tex
@@ -1,2 +1,2 @@
-\newcommand{\fclangversion}{DRAFT+\xspace}
+\newcommand{\fclangversion}{Chlorine+\xspace}
\newcommand{\fcversion}{Potassium+\xspace}
diff --git a/doc/userman/introduction.tex b/doc/userman/introduction.tex
index 337d6f3c..fbedaaec 100644
--- a/doc/userman/introduction.tex
+++ b/doc/userman/introduction.tex
@@ -6,14 +6,14 @@ language~\cite{acsl}. This manual documents the \fclang plug-in of \framac,
version \fclangversion.
The \fclang plug-in supports the \acslpp extension of \acsl for C++ programs and specifications;
it is built on the Clang\footnote{https://clang.llvm.org/} compiler infrastructure and uses Clang for
-parsing C++.
+parsing C++. The plug-in extends clang to parse \acslpp, translating it into an intermediate language for C and \acsl.
-The \fclang plug-in intends to provide a full translation of C++ and \acslpp into the \framac internal representation, and from there be able to be analyzed by other \framac plug-ins.
-This is a work in progress.
-The following sections describe the limitations of the current implementation.
+The \fclang plug-in intends to provide a full translation of C++ and \acslpp into the \framac internal representation, and from there to allow C++ progems 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 C++
- \item \acslpp is described in the companion \acslpp reference manual, also a part of the \framac release.
+ \item \acslpp is described in the companion \acslpp reference manual \cite[TODO], also a part of the \framac release.
\end{itemize}
diff --git a/doc/userman/main.tex b/doc/userman/main.tex
index 6ecb4f66..c089064b 100644
--- a/doc/userman/main.tex
+++ b/doc/userman/main.tex
@@ -18,14 +18,14 @@
\begin{document}
-\coverpage{\fclang User Manual}
+\coverpage{\fclang User Manual for \fclang version \fclangversion and \fc version \fcversion}
\begin{titlepage}
\begin{flushleft}
\includegraphics[height=14mm]{cealistlogo.jpg}
\end{flushleft}
\vfill
-\title{\fclang Plug-in}{Release \fclangversion
+\title{\fclang Plug-in User Manual}{Release \fclangversion
%% \ifthenelse{\equal{\eacslversion}{\fcversion}}{}{%
%% \\[1em] compatible with \framac \fcversion}
}
@@ -34,7 +34,7 @@
CEA LIST\\ Software Reliability \& Security Laboratory
\end{center}
\begin{center}
- Last modified \ddMyyyydate\today
+ Document printed \ddMyyyydate\today
\end{center}
\vfill
\begin{flushleft}
@@ -52,11 +52,11 @@ CEA LIST\\ Software Reliability \& Security Laboratory
\markright{}
\addcontentsline{toc}{chapter}{Foreword}
-This is the user manual of the \framac plug-in
+This is the user manual for the \framac plug-in
\fclang\footnote{\url{https://frama-c.com/frama-clang.html}}. The contents of this
-document correspond to its version \fclangversion compatible with
+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 may
+the \fclang plug-in is still ongoing. Features described by this document will certainly
evolve in the future.
\section*{Acknowledgements}
@@ -64,7 +64,7 @@ evolve in the future.
We gratefully thank the people who contributed to this document:
David R. Cok, Virgile Prevosto, Armand Pucetti, Franck Verdrine.
-This work is done in the context of project VESSEDIA,
+This document was written in the context of project VESSEDIA,
which received funding from the European Union's 2020
Research and Innovation Program under grant agreement
No. 731453.
diff --git a/doc/userman/preprocessing.tex b/doc/userman/preprocessing.tex
index eee212c4..545540c9 100644
--- a/doc/userman/preprocessing.tex
+++ b/doc/userman/preprocessing.tex
@@ -2,7 +2,7 @@
As a refresher, the C/C++ preprocessor (CPP) (cf. \url{https://gcc.gnu.org/onlinedocs/cpp/}) conceptually implements the following operations on a C++ source file:
\begin{itemize}
- \item The input is read and broken it into a sequence of physical lines according to the line terminators (ASCII character sequences \\r, \\n, or \\r\\n).
+ \item The input is read and broken it into a sequence of physical lines according to the line terminators (ASCII character sequences \texttt{\\r}, \texttt{\\n}, or \texttt{\\r\\n}).
\item Each C trigraph is replaced by its corresponding character.
\item Any backslash-whitespace-line-terminator sequence is removed and the line that it ends is combined with the following line.
\item Comments are replaced by single spaces. This requires tokenizing the input to avoid recognizing comment markers within strings as indicating a comment. Note that this allows block comments to hide line terminations.
@@ -31,7 +31,7 @@ Note that not all preprocessor tokens are valid C/C++ parser tokens. Tokens in t
\acsl and \acslpp have slightly different tokens than the above, so the preprocessor tokens need to be re-tokenized in some cases:
\begin{itemize}
- \item The \@ token is a whitespace character in \acslb.
+ \item The \texttt{\at} token is a whitespace character in \acslb.
\item There are some \acslb multi-character punctuator tokens that are not
preprocessor tokens:
\begin{itemize}
@@ -39,7 +39,9 @@ Note that not all preprocessor tokens are valid C/C++ parser tokens. Tokens in t
\item[] $-->$ (bit-wise implies)
\item[] $<==>$ (logical equality)
\item[] $<-->$ (bit-wise equality)
- \item[] TBD any more?
+ \item[] TODO (logical inequality)
+ \item[] TODO (list repetition)
+ \item[] TBD any more? [| |]
\end{itemize}
These \acslb tokens need to be assembled from multiple CPP tokens (and those CPP tokens must not be separated by white space)
\item A CPP numeric token that contains .. will not be a legal C/C++ number, but may be multiple legal \acslb tokens with the .. representing the range operator. For example, the single CPP token \texttt{0..last} is retokenized for \acslb as if it were written \texttt{0 .. last} .
@@ -84,7 +86,7 @@ Consequently, any directives contained in the annotation are not seen when the s
Accordingly, \acslpp imposes constraints on the directives that may be present within annotations:
\begin{itemize}
\item \texttt{define} and \texttt{undef} are not permitted in an annotation
- \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 \#endif and its corresponding \#if/\#ifdef/\#ifndef must be in the same annotation comment.)
+ \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 i\texttt{\#if/\#ifdef/\#ifndef} must 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, either \texttt{define} or \texttt{pragma} directives
\item \texttt{line} - TBD
--
GitLab