Skip to content
Snippets Groups Projects
Commit 8f9f90f4 authored by DavidCok's avatar DavidCok Committed by Virgile Prevosto
Browse files

Weekend edits

parent afd9caa3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 164 additions and 102 deletions
doc/userman/changes.tex
+ 1
− 7
View file @ 8f9f90f4
......@@ -3,13 +3,7 @@
This chapter summarizes the changes in this documentation between each \fclang
release, with the most recent releases first.
\begin{itemize}
\item New section \textbf{Additional Verifications}.
\item Update each section with respect to the changes introduced since \eacsl
Sulfur-20180101.
\end{itemize}
\section*{Frama-C Chlorine-20180101}
\section*{Version \fclangversion}
\begin{itemize}
\item First release of this manual.
......
doc/userman/description.tex
+ 55
− 15
View file @ 8f9f90f4
......@@ -2,7 +2,28 @@
\chapter{Installation}
TBD - installation instructions
\fclang is currently still experimental and not part of regular \framac releases. It must be built from source and added to a \framac installation.
The instructions for doing so are provided at
\url{https://frama-c/colm/frama-clang.html}.
\fclang depends on two software packages:
\begin{itemize}
\item A current version of \framac itself
\item An installation of Clang, which is available as part of LLVM,
which itself is available from \url{http://releases.llvm.org}.
\end{itemize}
Building and installing \fclang has two effects:
\begin{itemize}
\item The \fclang executable files are installed within the \framac installation
\item The include files containing \acslpp specifications of C++ library functions
are copied to \verb|$FRAMAC_SHARE/libc| and
\verb|$FRAMAC_SHARE/libc++|, where \verb|$FRAMAC_SHARE| is the path
given by the command \lstinline|frama-c-config -print-share-path|.
\end{itemize}.
These include files are replacements for the standard system include files.
They should have the same definitions of C and C++ functions and classes, but
with \acslpp annotations giving their specifications.
\chapter{Running the plug-in}
......@@ -16,7 +37,8 @@ reinstalling the plugin.
\section{Frama-clang executable}
The plug-in operates by invoking the executable \irg
on each file identified as C++, in turn.
For each file it produces a temporary output file containing the C AST, which is then given as input to frama-c. This executable is a single-file-at-a-time command-line executable only.
For each file it produces a temporary output file containing the C AST, which is then given as input to \framac.
This executable is a single-file-at-a-time command-line executable only.
Various options control its behavior.
The file-system path identifying the executable is provided by the \textbf{-cxx-clang-command <cmd>}
......@@ -25,6 +47,14 @@ option and is \irg by default. The path may be absolute; if it is a relative pat
\section{Frama-clang options}
The options controlling \fclang are of two sorts:
\begin{itemize}
\item options known to \framac are interpreted and passed on to \fclang when
\irg is invoked, perhaps with a different option name
\item options known to \fclang directoy (and not ot \framac) must be
included in the internal command that invokes \irg using the \option{-cpp-extra-args} option. These options are described in \S\ref{sec:standalone}.
\end{itemize}
The options known to the \fcl plugin are processed by the \fc kernel when listed on the \fc command-line.
The use of the \fc command-line is described in the core \fc
user guide.
......@@ -61,13 +91,22 @@ TODO
TODO
\chapter{Running the frama-clang front-end standalone}
\section{Controlling output}
TODO
- make warnings errors
- stop om first error
- supplying an exisintg IRG file to frama-c
In normal use within \fc, the \irg executable is
\chapter{Running the \fclang front-end standalone}
\label{sec:standalone}
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 file;
it produces a C AST representing the translated C++, in a text format
of the CIL (C Intermediate language). [TODO - or is it CABS]
of the CIL (C Intermediate language).
\section{Clang options}
......@@ -83,7 +122,7 @@ You can see a list of options by running
The most significant options for \irg 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 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{-o <file>} -- specifies the 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.
\item \option{-std=...} -- the input programming language (default is \lstinline|-std=c++11|)
\item \option{-w} -- suppress warnings
\item \option{-{-}version} -- print version information
......@@ -94,23 +133,24 @@ The most significant options for \irg are these:
There are also options that are specific to \fcl.
These are listed below:
\begin{itemize}
\item \option{-{-}stop-annot-error} -- if set, then parsing stops on the first error; default is off
\item \option{-{-}gen-impl-method} -- TODO
\item \option{-{-}exit-code} -- if set, then the exit code of \irg is 1 if errors occur; this is not the default because then \lstinline|frama-c| would terminate upon
any error in \lstinline|framaCIRGen|
\item \option{-{-}no-exit-code} -- disables \option{-{-}exit-code}
\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;
\option{-{-}no-info} sets the level to 0. The \lstinline|frama-c| option \option{-fclang-msg-key=parse} is equivalent to setting a value of 1.
\item \option{-{-}warn=<n>} -- sets the level of parser warning messages to \textbf{n}; 0 is completely quiet; increasing values are
more verbose. \option{-{-}warn} sets the level to 1;
\option{-{-}no-warnyyp} sets the level to 0. The \lstinline|frama-c| option \option{-fclang-warn-key=parse} is equivalent to setting a value of 1.
\option{-{-}no-warn} sets the level to 0. The \lstinline|frama-c| option \option{-fclang-warn-key=parse} is equivalent to setting a value of 1.
\item \option{-{-}debug=<n>} -- sets the level of parser debug messages to \textbf{n}; 0 is completely quiet; increasing values are
more verbose. \option{-{-}debug} sets the level to 1;
\option{-{-}no-debug} sets the level to 0. The \lstinline|frama-c| option \option{-fclang-debug=<n>} is equivalent to setting a value of \textbf{n}.
In particular, a debug value of 1 shows the command-line that invokes
\irg.
\option{-{-}no-debug} sets the level to 0.
The \lstinline|frama-c| option \option{-fclang-debug=<n>} is equivalent to setting a value of \textbf{n}.
In particular, a debug value of 1 shows the command-line that invokes \irg.
\item \option{-{-}stop-annot-error} -- if set, then parsing stops on the first error; default is off
\item \option{-{-}gen-impl-method} -- TODO
\item \option{-{-}exit-code} -- if set, then the exit code of \irg is 1 if errors occur; this is not the default because then \lstinline|frama-c| would terminate upon
any error in \lstinline|framaCIRGen|
\item \option{-{-}no-exit-code} -- disables \option{-{-}exit-code}, so that the exit code is always 0.
\item TODO: -b -x -o -v
\end{itemize}
......
doc/userman/eacslversion.tex deleted 100644 → 0
+ 0
− 2
View file @ afd9caa3
\newcommand{\eacslversion}{Chlorine-20180501+dev\xspace}
\newcommand{\fcversion}{Chlorine\xspace}
doc/userman/fclangversion.tex
+ 2
− 1
View file @ 8f9f90f4
\newcommand{\fclangversion}{Chlorine+\xspace}
\newcommand{\version}{0.1\xspace}
\newcommand{\fclangversion}{DRAFT\xspace}
\newcommand{\fcversion}{Potassium+\xspace}
doc/userman/grammar.tex 0 → 100644
+ 23
− 0
View file @ 8f9f90f4
\newcommand{\lang}{C++}
\section{Grammar}
\label{sec:grammar}
This section summarizes some of the considerations in writing a parser for \acslpp within \fclang.
Recall that \fclang uses clang to parse \lang and a custom parser to parse \acslpp annotations, jointly producing a representation of the \lang+\acslpp source input in the Frama-C intermediate language. The first version of the \acslpp custom parser, swritten 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 change 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, and name lookup and type resolution.
The new parser uses a recursive descent design inn 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. The offending features are mostly inherited from \lang. The next few subsections describe the problematic aspects of \acslpp and how they are addressed.
The principal goal of an LL(k) forumulation 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.
\begin{itemize}
\item \textbf{Left recursion}. Expression grammars are typically left recursive. However, it is well-known how to factor out left recursion. The precedence order of operators is largely hard-coded into the grammar implementation; the usual left recursion poses no particular challenge.
\item {terms vs. predicates}. \acslpp distinguishes terms and predicates, following the distinction between propositional and predicate logic. However, terms and predicates have very similar grammars. Furthermore, \acslpp allows boolean-value terms to be implicitly converted to predicates and allows predicates to be used within terms (such as for the conditional sub-expression in a ternary expression). This makes it not possible to distinguish terms and predicates inn top-down parsing. However, Frama-C has different AST nodes for the two, so it would require a very significant refactoring of Frama-C and all its plugins to unify terms and predicates (as other specification languages have done). Note that this problem is a challenge for any parser design. The previous and current parser designs adopted the same solution; maintain two parallel parses of expressions --- one as a term and one as a predicate. Error messages are emitted only when both parses fail or when a particular grammar production call for a particular type (term or predicate) and that one is not available.
\item{terms vs. tsets}. TODO
\item \textbf{cast vs. parenthesized expression} To determine whether an input like \lstinline|(T)+x| is (a) the sum 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 reqwuires 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. 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 set comprehension expression follows traditional mathematics: \lstinline| { \textit{expr} | \textit{binders} ; \textit{predicate} . This structure poses two difficulties for parsers. First, the expression 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 LALR 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{labeled expressions}. \acslpp allows expressions to have labels, designated by a \lstinline|id : | prefix. Thus the parser cannot know whether an initial \lstinline|id| is a variable or just a label until the colon is parsed. Thus this situation requires a lookahead of 2 tokens.
\end{itemize}
doc/userman/introduction.tex
+ 6
− 26
View file @ 8f9f90f4
\chapter{Introduction}
\framac~\cite{userman,fac15} is a modular analysis framework for the C
programming language which supports the \acsl specification
programming language that supports the \acsl specification
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;
......@@ -13,30 +13,10 @@ The \fclang plug-in intends to provide a full translation of C++ and \acslpp int
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 \cite[TODO], also a part of the \framac release.
\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 8 of Clang.
This version of Clang supports C++ versions through C++17
(cf. \url{https://clang.llvm.prg/cxx_status.;html}.
However, \fclang may not support all of the features of C++ within annotations.
\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}
%The \fclang version you are using is indicated by the
%command \texttt{frama-c -e-acsl-version}\optionidx{-}{e-acsl-version}. \fclang
%automatically translates an annotated C program into another program that fails
%at runtime if an annotation is violated. If no annotation is violated, the
%behavior of the new program is exactly the same as the one of the original
%program.
%This manual does \emph{not} explain how to install the \eacsl plug-in. For
%installation instructions please refer to the \texttt{INSTALL} file in the
%\eacsl distribution. \index{Installation} Furthermore, even though this manual
%provides examples, it is \emph{not} a full comprehensive tutorial on
%\framac or \eacsl.
% You can still refer to any external
% tutorial~\cite{rv13tutorial} for additional examples.
doc/userman/limitations.tex
+ 22
− 1
View file @ 8f9f90f4
\chapter{Known Limitations}
The development of the \fclang plug-in is still ongoing.
The development of the \fclang plug-in is still ongoing.
\fclang does not implement all of current C++ nor all of
\acslpp as defined in its language definition.\cite{acslpp}
The mosty important such limitations are described in this section.
\section{Implementation of C++}
The following are not implemented in \acslpp.
\begin{itemize}
\item \acslpp definitions within template declarations
\item digraphs within \acslpp annotations
\item preprocessing is restricted within \acslpp annotations (cf. \S\ref{sec:preprocessing})
\end{itemize}
\section{Implementation of \acslpp}
\begin{itemize}
\item ghost declarations
\item model declarations
\item set comprehensions
\end{itemize}
doc/userman/macros.tex
+ 4
− 3
View file @ 8f9f90f4
......@@ -5,10 +5,11 @@
\usepackage{comment}
\newcommand{\framac}{\textsc{Frama-C}\xspace}
\newcommand{\fclang}{\textsc{Frama-Clang}\xspace}
\newcommand{\acsl}{\textsc{ACSL}\xspace}
\newcommand{\eacsl}{\textsc{E-ACSL}\xspace}
\newcommand{\acslpp}{\textsc{ACSL++}\xspace}
\newcommand{\acslb}{\acsl/\acslpp\xspace}
\newcommand{\eacslgcc}{\texttt{e-acsl-gcc.sh}\xspace}
\newcommand{\rte}{\textsc{RTE}\xspace}
\newcommand{\C}{\textsc{C}\xspace}
\newcommand{\jml}{\textsc{JML}\xspace}
......@@ -45,7 +46,7 @@
\newcommand{\todo}[1]{{\large \textbf{TODO: #1.}}}
\newcommand{\option}[1]{\textbf{#1}}
\newcommand{\irg}{\lstinline|framaCIRGen|i\xspace}
\newcommand{\irg}{\lstinline|framaCIRGen|\xspace}
\newcommand{\fcl}{\lstinline|frama-clang|\xspace}
\newcommand{\fc}{\lstinline|frama-c|\xspace}
......
doc/userman/main.tex
+ 6
− 11
View file @ 8f9f90f4
......@@ -8,9 +8,6 @@
\include{macros}
\newcommand{\fclang}{\textsc{Frama-Clang}\xspace}
\newcommand{\acslpp}{\textsc{ACSL++}\xspace}
\newcommand{\acslb}{\acsl/\acslpp\xspace}
\include{fclangversion}
......@@ -18,14 +15,14 @@
\begin{document}
\coverpage{\fclang User Manual for \fclang version \fclangversion and \fc version \fcversion}
\coverpage{\fclang User Manual \\ version \version{} \\for \fclang version \fclangversion \\and \framac version \fcversion}
\begin{titlepage}
\begin{flushleft}
\includegraphics[height=14mm]{cealistlogo.jpg}
\end{flushleft}
\vfill
\title{\fclang Plug-in User Manual}{Release \fclangversion
\title{\fclang Plug-in User Manual}{Release \version for \fclang \fclangversion
%% \ifthenelse{\equal{\eacslversion}{\fcversion}}{}{%
%% \\[1em] compatible with \framac \fcversion}
}
......@@ -38,7 +35,7 @@ CEA LIST\\ Software Reliability \& Security Laboratory
\end{center}
\vfill
\begin{flushleft}
\textcopyright 2013-2018 CEA LIST
\textcopyright 2013-2019 CEA LIST
%%
%% This work has been supported by the VESSEDIA project).
\end{flushleft}
......@@ -62,7 +59,7 @@ evolve in the future.
\section*{Acknowledgements}
We gratefully thank the people who contributed to this document:
David R. Cok, Virgile Prevosto, Armand Pucetti, Franck Verdrine.
David R. Cok, Virgile Prevosto, Armand Puccetti, Franck Verdrine.
This document was written in the context of project VESSEDIA,
which received funding from the European Union's 2020
......@@ -76,11 +73,9 @@ No. 731453.
\include{description}
\include{limitations}
\include{preprocessing}
\include{preprocessing}http://web.ift.uib.no/Teori/KURS/WRK/TeX/symALL.html
\include{grammar}
\section{\acslpp constructs}
\textit{This section is not yet written}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
doc/userman/preprocessing.tex
+ 43
− 36
View file @ 8f9f90f4
\section{Preprocessing}
\chapter{Preprocessing}
This section describes the implementation of the C++ preprocessor for \acslpp
annotations. Recall that thte C++ preprocessor replaces comments (including
\acslpp comments) by white space, without operations such as handling
preprocessor directives. Accordingly, \fclang must handle standard
preprocessing within \acslpp annotations itself.
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}
......@@ -8,6 +14,7 @@ As a refresher, the C/C++ preprocessor (CPP) (cf. \url{https://gcc.gnu.org/onlin
\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.
\item The input text is divided into preprocessing tokens grouped in logical lines. Each preprocessor token becomes a compiler token (except where \#\# concatenation occurs). However, \acslb tokens are slightly different, as described below.
\item The source text is transformed according to any preprocessing directives contained within it. Each preprocessing directive must be contained within one logical line
\item adjacent string literals (separatedonly by white-space or line-endings) are concatenated into a single string literal.
\end{itemize}
The result is a sequence of preprocessing tokens that is passed on to the
......@@ -17,59 +24,59 @@ remaining compiler phases.
TBD - are these supported by clang?
\subsection{Digraphs}
Digraphs are alternate spellings of preprocessort tokens, in particular, of
punctuation character sequences. No digraphs are defined in \acslpp for use
in \acslpp annotations.
\subsection{Preprocessor tokens}
Preprocessor tokens (per CPP) belong to one of five categories. White space (space, tab, TBD) 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.
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 \texttt{[a-zA-Z\_][a-zA-Z\_0-9]*} . Dollar signs are allowed as non-digit identifier characters if the clang option \texttt{-fdollars-in-identifiers} is used. (TBD - on by default?)
\item number: character sequences that match the regular expression \texttt{[.]?[0-9]([0-9a-zA-Z.]|[eEpP][+-]))*} . (TBD - dollar signs also allowed?)
\item identifiers: character sequences that match the regular expression \\
\centerline{\texttt{[a-zA-Z\_][a-zA-Z\_0-9]*}} .\\ Dollar signs are allowed as non-digit identifier characters if the clang option \texttt{-fdollars-in-identifiers} is used. (TBD - on by default?)
\item number: character sequences that match the regular expression \\
\centerline{\texttt{[.]?[0-9]([0-9a-zA-Z.]|[eEpP][+-]))*}} . \\
(TBD - dollar signs also allowed?)
\item string literals: character sequence enclosed in " " or ' ' or < >, with \textbackslash " for " in a double-quoted literal (that is not a header file name) and \' for ' in a single-quoted literal.
\item punctuator: all single non-alphanumeric printable characters except \@, \# and `, and all multi-punctuation sequences that meaningful to C/C++ (e.g. >>>= ), but not an arbitrary multi-punctuation character sequence.
\\item other tokens: \@, \#, ` and all non-ASCII single characters.
\item punctuator: all single non-alphanumeric printable characters except
\verb|@|, \verb|#| and \verb|`|, and all multi-punctuation sequences that meaningful to C/C++ (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}
TBD - unicode characters
The above token definitions imply that arbitrary text can always be broken into
legitimate tokens, with the exception of a few characters and of badly formed unicode sequences.
TODO - unicode characters
Note that not all preprocessor tokens are valid C/C++ parser tokens. Tokens in the other category have no meaning to C/C++ and the \texttt{number} category allows many sequences that are not legal C/C++ numeric tokens. These tokens will generally provoke compiler errors. For example in C/C++, 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:
\begin{itemize}
\item The \texttt{\at} token is a whitespace character in \acslb.
\item The \verb|@| token is a whitespace character in \acslb.
\item There are some \acslb multi-character punctuator tokens that are not
preprocessor tokens:
single preprocessor tokens:
\begin{itemize}
\item[] all \acslb keywords that begin with a backslash, such as
\verb|\result|.
\item[] $==>$ (logical implies)
\item[] $-->$ (bit-wise implies)
\item[] $<==>$ (logical equality)
\item[] $<-->$ (bit-wise equality)
\item[] TODO (logical inequality)
\item[] TODO (list repetition)
\item[] TBD any more? [| |]
\item[] \verb|^^| (logical inequality)
\item[] \verb|^*| (list repetition)
\item[] \verb:[|: and \verb:|]: (list creation)
\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} .
\item \acslb allows certain built-in non-ASCII symbols, namely
\begin{itemize}
\item[] $\forall$ (unicode 0x2200) - universal quantifier
\item[] $\exists$ (unicode 0x2203) - existential quantifier
% \item[] $\equal$ (unicode 0x2261) - equality
% \item[] $\notequal$ (unicode 0x2262) - inequality
\item[] $\leq$ (unicode 0x2264) - less than or equal
\item[] $\geq$ (unicode 0x2265) - greater than or equal
% \item[] $\minus$ (unicode 0x2212) - minus
% \item[] $\implies$ (unicode 0x21D2) - implies
% \item[] $\equiv$ (unicode 0x21D4) - equivalence
\item[] $\bigwedge$ (unicode 0x2227) - logical and
\item[] $\bigvee$ (unicode 0x2228) - logical or
\item[] $\neg$ (unicode 0x00AC) - logical negation
% \item[] $\logicalxor$ (unicode 0x22BB) - logical inequivalence
\item[] $\subset$ (unicode 0x2208) - subset
% \item[] $\Boolean$ (unicode 0x1D539) - set of booleans
% \item[] $\Integer$ (unicode 0x2124) - set of integers
% \item[] $\Real$ (unicode 0x211D) - set of reals
\item TBD - more - ensure unicode equivalent
\end{itemize}
\item A CPP numeric token that contains .. will not be a legal C/C++ number, but may be a sequence of
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} .
\item \acslb allows certain built-in non-ASCII symbols.
An example is
$\forall$ (unicode 0x2200) x to designate a universal quantifier,
which is an alternative form of \verb|\forall|.
A complete list of such tokens is given in the \acslb language definition.
\end{itemize}
\subsection{Preprocessor directives}
A preprocessing directive consists of a line (after the previous preprocessing phaseshave been completed) that begins with optional white space, the '\#' character, additional optional white space, and a preprocessor directive identifier.
A preprocessing directive consists of a single logical line (after the previous preprocessing phases have been completed) that begins with optional white space, the '\#' character, additional optional white space, and a preprocessor directive identifier.
The preprocessing language contains a fixed set of preprocessing directive identifiers:
\begin{itemize}
\item \texttt{define}, \texttt{undef}
......@@ -86,7 +93,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 \texttt{\#endif} and its corresponding i\texttt{\#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 \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
......
doc/userman/version.tex 0 → 100644
+ 2
− 0
View file @ 8f9f90f4
\newcommand{\fclangversion}{Chlorine+\xspace}
\newcommand{\fcversion}{Potassium+\xspace}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment