From 963c9717edc73b53534362be05f011d8a54f315b Mon Sep 17 00:00:00 2001
From: davidcok <davidcok@github.com>
Date: Tue, 6 Aug 2019 15:29:00 +0200
Subject: [PATCH] more editing
---
doc/userman/description.tex | 6 ++++--
doc/userman/limitations.tex | 17 +++++++++++++----
doc/userman/macros.tex | 2 +-
doc/userman/main.tex | 4 ++--
doc/userman/preprocessing.tex | 2 +-
5 files changed, 21 insertions(+), 10 deletions(-)
diff --git a/doc/userman/description.tex b/doc/userman/description.tex
index 3e68c71c..687a7c0d 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 588716fb..b19b634f 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 654de0ce..a0bcc851 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 214a3df6..b4d73269 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 421c930d..c8963893 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
--
GitLab