Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • pub/frama-clang
  • weliveindetail/frama-clang
  • ankit247/frama-clang
  • T-Gruber/frama-clang
4 results
Show changes
Hide whitespace changes
Inline Side-by-side
Showing
with 891 additions and 413 deletions
doc/userman/description.tex
View file @ 54b2bdf8
\chapter{Installation}
\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.com/frama-clang.html}.
\framaclang is currently still experimental and not part of regular \FramaC releases. It must be built from source and added to a \FramaC installation.
If you're already using the \opam package manager to install \FramaC (see below),
\framaclang can be installed directly with \lstinline|opam install frama-clang|.
\fclang depends on two software packages:
The remainder of this chapter gives the instructions for installing \framaclang manually.
\framaclang depends on two software packages:
\begin{itemize}
\item A current version of \framac itself. It is highly recommended to install \framac using \lstinline|opam|, as described in the installation procedures for \framac (\url{https://frama-c.com/download.html}).
Version \fclangversion of \fclang is compatible with version \fcversion of \framac.
\item A current version of \FramaC itself. It is highly recommended to install \FramaC using \lstinline|opam|, as described in the installation procedures for \FramaC (\url{https://frama-c.com/download.html}).
Version \fclangversion of \framaclang is compatible with version \framacversion of \FramaC.
\item An installation of Clang, which is available as part of LLVM,
which itself is available from \url{http://releases.llvm.org}.
Version \fclangversion of \fclang is compatible with version \clangversion of \clang.
which itself is available from \url{http://releases.llvm.org}. Note that you will need
\clang's library and its headers, not just the compiler itself.
Version \fclangversion of \framaclang is compatible with version \clangversion of \clang.
\end{itemize}
Building and installing \fclang has two effects:
In addition, a third package is needed for compiling \framaclang,
\lstinline|camlp5| (\url{https://camlp5.github.io/}).
Once \framaclang has been installed, \lstinline|camlp5| is not required anymore.
Again, the easiest way to install
\lstinline|camlp5| itself is through \lstinline|opam|. Finally, newer versions
of OCaml have dropped the \lstinline|Genlex| and \lstinline|Streams| modules
from their standard library, so that another \lstinline|opam| package must be
installed as well, namely \lstinline|camlp-streams|.
Building and installing \framaclang has three effects:
\begin{itemize}
\item The \fclang executable files are installed within the \framac installation.
In particular, if \framac has been installed using \lstinline|opam|, then the principal executable \irg will be installed in the
\lstinline|opam| \lstinline|bin| directory.
You must be sure that this directory is on your system \verb|$PATH| (try \lstinline|which framaCIRGen| after installation to be sure).
\item Include files containing \acslpp specifications of \cpp library functions
are copied to \verb|$FRAMAC_SHARE/libc| and
\item The \framaclang executable files are installed within
the \FramaC installation.
In particular, if \FramaC has been installed using \lstinline|opam|,
then the principal executable \irg will be installed in the
\lstinline|opam| \lstinline|bin| directory.
You must be sure that this directory is on your \verb|$PATH|.
This is usually the default for standard \lstinline|opam| installations.
In doubt, you can try the command \lstinline|which framaCIRGen|
after installation to be sure that \irg will be correctly detected by your
shell.
\item The \FramaC plug-in itself is copied into the standard \FramaC plug-in
directory (as given by \lstinline|frama-c-config -print-plugin-path|), so
that it will be loaded automatically by the main \FramaC commands at each
execution.
\item Include files containing \acslpp specifications of \Cpp library functions
are copied to directory
\verb|$FRAMAC_SHARE/frama-clang/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 \cpp functions and classes, but
with \acslpp annotations giving their specifications.
These include files are replacements for (a subset of)
the standard system include files. They should have the same definitions of
\C and \Cpp functions and classes, but
with \acslpp annotations giving their specifications. Note however that this is
still very much a work in progress, except for the headers that are imported
from the C standard library, which benefit from the specifications of the
headers provided by \FramaC itself.
The plugin can be built by hand from source using the following commands. Create a new directory to which you download and unpack the source distribution. Then \lstinline|cd| into the source directory itself (one level down) and execute:
\begin{listing-nonumber}
./configure
make
make install
\end{listing-nonumber}
By default, \fclang will install its files under the same root
directory as \framac itself. In particular, if \framac has been
By default, \framaclang will install its files under the same root
directory as \FramaC itself. In particular, if \FramaC has been
installed from \lstinline|opam|, the installation will be done under
\verb|$(opam var prefix)| directory. Standard configure options for
manipulating installation directories are available, notably
\verb|--prefix|.
\verb|$(opam var prefix)| directory. To install it in another directory,
you can set the \lstinline|PREFIX| environment variable before executing
\lstinline|make install|. Note that in that case, \FramaC may not be able
to load the plug-in automatically.
%\section{Current status}
%
%Currently on Ubuntu 17.10 and MacOSX (Sierra 10.12.6), \fclang builds in this configuration:
%Currently on Ubuntu 17.10 and MacOSX (Sierra 10.12.6), \framaclang builds in this configuration:
%
%\begin{itemize}
%\item Install opam (>= 2.0)
......@@ -64,24 +87,27 @@ manipulating installation directories are available, notably
%
%
%\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 \framaclang 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
%\item \framaclang 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}
Once installed the plugin is run automatically by \framac on any \cpp files listed on the command-line. \cpp files are identified by their filename suffixes. The default suffixes recognized as \cpp are these:
\section{\Cpp files}
Once installed the plugin is run automatically by \FramaC on any \Cpp
files listed on the command-line. \Cpp files are identified by their
filename suffixes. The default suffixes recognized as \Cpp are these:
\lstinline| .cpp, .C, .cxx, .ii, .ixx, .ipp, .i++, .inl, .h, .hh|
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.
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}
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 an equivalent \C AST, which is then translated and passed on as input to \framac.
on each file identified as \Cpp, in turn.
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.
......@@ -89,69 +115,113 @@ The file-system path identifying the executable is provided by the \textbf{-cxx-
option and is \irg by default. The path may be absolute; if it is a relative path, it is found by searching the system \verb|$PATH|.
The PARSING section of the output of \lstinline|frama-c -kernel-h| lists some options for controlling the behavior described above. Also see the options listed by \lstinline|frama-c -fclang-h| such as \lstinline|-cxx-stdlib-path|, \lstinline|-cxx-cstdlib-path|, \lstinline|-cxx-nostdinc|, \lstinline|-cxx-stdinc|.
The PARSING section of the output of \lstinline|frama-c -kernel-h|
lists some options for controlling the behavior described above. This is notably
the case for:
\begin{itemize}
\item \lstinline|-cpp-extra-args| which contains arguments to be passed to the
preprocessor (e.g. \lstinline|-D| macro definitions or \lstinline|-I|
search path directives). In case the project under analysis mixes C and
C++ files which
require distinct preprocessor directives, it is possible to use the
\framaclang-specific option \lstinline|-fclang-cpp-extra-args|.
In that case, \framaclang will not consider \lstinline|-cpp-extra-args| at all.
See section~\ref{sec:include-directories} for more information.
\item \lstinline|-machdep| which indicates the architecture on
which the program is supposed to run. See section~\ref{sec:bit} for more
information
\end{itemize}
Apart from \lstinline|-fclang-cpp-extra-args|, and
\lstinline|-cxx-clang-command|, \framaclang options governing the
parsing of C++ files are:
\begin{itemize}
\item \lstinline|-cxx-c++stdlib-path|, the path where \framaclang standard C++
headers are located.
\item \lstinline|-cxx-cstdlib-path|, the path where \FramaC standard C headers
are located
\item \lstinline|-cxx-nostdinc|, instructs \irg not to consider \framaclang and
\FramaC headers (i.e. fall back to system headers).
\end{itemize}
\section{Frama-clang options}
The options controlling \fclang are of four sorts:
The options controlling \framaclang are of four sorts:
\begin{itemize}
\item options known to the \framac kernel
\item options the \fclang plug-in has registered with the \framac kernel. These also are recognized by the \fc command-line.
\item options known to \irg directly (and not to \fc), These 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}.
\item \clang options, which must also be supplied using the \option{-cpp-extra-args} option, and are passed through \irg to \cl. See \S\ref{sec:standalone}.
\item options known to the \FramaC kernel
\item options the \framaclang plug-in has registered with the \FramaC kernel.
These also are recognized by the FramaCcommand-line.
\item options known to \irg directly (and not to FramaC, These must be
included in the internal command that invokes \irg using the \lstinline|-cpp-extra-args| option. These options are described in \S\ref{sec:standalone}.
\item \clang options, which must also be supplied using the \lstinline|-cpp-extra-args| option, and are passed through \irg to \clang. See \S\ref{sec:standalone}.
\end{itemize}
The options in the first two categories 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
The options in the first two categories are processed by the \FramaC kernel
when listed on the \FramaC command-line.
The use of the FramaCcommand-line is described in the core \FramaC
user guide.
There are many kernel options that affect all plugins and many options specific to \fclang.
There are many kernel options that affect all plugins and many options specific to \framaclang.
The command \\
\centerline{\lstinline|frama-c -kernel-h|} \\
shows all kernel options; the command\\
\centerline{\lstinline|frama-c -fclang-h|} \\
shows all \fcl-specific options.
shows all \framaclang specific options.
The most important of the options are these:
\begin{itemize}
\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
important for adding include directories (\lstinline|-I|) and
other options to be passed on to the clang compiler or the \irg executable.
Multiple instances of this option have a cumulative effect, in order (rather
than later instances replacing earlier ones).
\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.
\item \lstinline|--help| or \lstinline|-h| -- introduction to \FramaC help
\item \lstinline|-kernel-h|, \lstinline|-fclang-h| -- help information about FramaC the FramaCkernel and the \framaclang plug-in
\item \lstinline|-print| -- prints out the input file seen by FramaC when
\framaclang 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 \framaclang's transformations.
\item \lstinline|-kernel-warn-key=annot-error=<val>| sets the behavior of \FramaC, including \framaclang, 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 \lstinline|-machdep <arg>| -- sets the target machine architecture, cf. \S\ref{sec:bit}
\item \lstinline|-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-warn-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.
\item \lstinline|-kernel-warn-key <categories>| -- sets the amount and behavior of warnings.\\ See \lstinline|-kernel-warn-key help| for a list of warning categories.
\item \lstinline|-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-warn-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)
\item \option{-no-annot} -- disables processing \acslpp annotations
\item \lstinline|-fclang-warn-key <categories>| -- sets the amount and behavior of warnings.\\ See \lstinline|-fclang-warn-key help| for a list of warning categories.
\item \lstinline|-fclang-verbose <n>| -- sets the amount of information
from the \framaclang plug-in
\item \lstinline|-fclang-debug <n>| -- sets the amount of debug
information from the \framaclang plug-in
\item \lstinline|-annot| -- enables processing \acslpp annotations (enabled by default)
\item \lstinline|-no-annot| -- disables processing \acslpp annotations
\item \lstinline|-cxx-unmangling <key>| indicates how mangled C++ symbols will be displayed
by \FramaC pretty-printing. \texttt{key} can be one of:
\begin{itemize}
\item \texttt{help}: outputs the list of existing \texttt{key} with a short description
\item \texttt{fully-qualified}: each symbol is displayed with its fully-qualified
C++ name
\item \texttt{without-qualifier}: each symbol is displayed with its unqualified name.
This gives shorter, but more ambiguous outputs.
\item \texttt{none}: no demangling is performed, symbols are displayed as seen in
the AST
\end{itemize}
\item \lstinline|-cxx-parseable-output| indicates that the pretty-printed code resulting
from the translation should be able to be parsed again by \FramaC. This implies
\lstinline|-cxx-unmangling none|.
\end{itemize}
Note that the \framac option \verb|-no-pp-annot| is ignored by \fclang. Preprocessing is always performed on the source input (unless annotations are ignored entirely using \verb|-no-annot|).
\section{Include directories}
Note that the \FramaC option \verb|-no-pp-annot| is ignored by \framaclang. Preprocessing is always performed on the source input (unless annotations are ignored entirely using \verb|-no-annot|).
\section{Include directories}\label{sec:include-directories}
By default \irg is given the paths to the two directories containing the \fcl and \fc header files, which include \acslpp specifications for the \cpp library functions. The default paths (\verb|$FRAMAC_SHARE/libc++| and
\verb|$FRAMAC_SHARE/libc| respectively) to these directories
can be overriden by the \fcl options \lstinline|-cxx-c++stdlib-path| and\\
By default \irg is given the paths to the two directories containing the
\framaclang and \FramaC header files, which include \acslpp specifications for the \Cpp library functions. The default paths (namely \verb|$FRAMAC_SHARE/libc++| and
\verb|$FRAMAC_SHARE/libc|) to these directories
can be overriden by the \framaclang options \lstinline|-cxx-c++stdlib-path| and
\lstinline|-cxx-cstdlib-path| options.
Users typically have additional header files for their own projects. These are supplied to the \fcl preprocessor using the option \lstinline|-cpp-extra-args|.
Users typically have additional header files for their own projects.
These are supplied to the \framaclang preprocessor using the option \lstinline|-cpp-extra-args|.
You can use \lstinline|-fclang-cpp-extra-args| instead of \lstinline|cpp-extra-args|; multiple such options also have a cumulative effect.
The \fcl option only affects the \fcl plugin, whereas
The \framaclang option only affects the \framaclang plugin, whereas
\lstinline|-cpp-extra-args| may be seen by other plugins as well, if such plugins do their own preprocessing. Also note that the presence of any instance of \lstinline|-fclang-cpp-extra-args| will cause uses of \lstinline|-cpp-extra-args| to be ignored.
The system header files supplied by \fcl does not include all \cpp system files. Omissions should be reported to the \fc team.
The system header files supplied by \framaclang does not include all \Cpp system files. Omissions should be reported to the \FramaC 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{\texttt{frama-c -cpp-extra-args="-Iinc" -wp a.cpp}}
......@@ -160,22 +230,26 @@ As an example, to perform \lstinline|wp| checking of files \lstinline|a.cpp| and
\label{sec:bit}
\acslpp is for the most part machine-independent.
There are some features of \cpp that can be environment-dependent, such as the sizes of fundamental datatypes.
Consequently, \framac has some options that allow the user to state what machine target is intended.
There are some features of \Cpp that can be environment-dependent, such as the sizes of fundamental datatypes.
Consequently, \FramaC has some options that allow the user to state what machine target is intended.
\begin{itemize}
\item The \option{-machdep} option to \framac. See the allowed values using the command\\
\item The \lstinline|-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=...|
For example, with a value of \lstinline|x86_32|, \lstinline|sizeof(long)| has a value of 4, whereas with the option \lstinline|-machdep x86_64|, \lstinline|sizeof(long)| has a value of 8.
%%\item Alternately, the value of \lstinline|-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}
\section{Warnings, errors, and informational output}
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 arise from multiple places: from the \framaclang 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 \clang 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.
......@@ -185,56 +259,53 @@ 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|--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|-kernel-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}.
\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 \Cpp code
\item \lstinline|-kernel-warn-key=annot-error=abort| is a \framaclang 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}
\subsection{Warnings}
%The various categories of warnings from \fcl can be seen with the command \\ \centerline{\lstinline|frama-c -fclang-warn-key help|}
%The various categories of warnings from \framaclang can be seen with the
%command \\ \centerline{\lstinline|frama-c -fclang-warn-key help|}
%Warning messages are emitted by default.
Warning messages from \irg can be controlled with the \lstinline|-warn| option of \irg.
% Note in the current version
%, or, equivalently, the \lstinline|-fclang-warn-key=parse| option of \fc.
%, or, equivalently, the \lstinline|-fclang-warn-key=parse| option of FramaC
\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|
% Cf above.
%\item the \fc option \lstinline|-fclang-warn-key=parse=inactive| is the same as the \irg option \lstinline|--warn=0|
%\item the \fc option \lstinline|-fclang-warn-key=parse=active| is the same as the \irg option \lstinline|--warn=1|
\end{itemize}
\textit{The \clang options are not currently integrated with the \fc warning and error key system.}
\textit{The \clang options are not currently integrated with the \FramaC
warning and error key system.}
\subsection{Informational output}
\textit{This section is not yet written}
\textit{The clang informational output is not currently integrated with the \fc warning and error key system.}
\textit{The \clang informational output is not currently integrated with the
\FramaC warning and error key system.}
\chapter{Running the \fclang front-end standalone}
\chapter{Running the \framaclang front-end standalone}
\label{sec:standalone}
In normal use within \framac, the \irg executable is
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 a text format similar to Cabs.
it produces a C AST representing the translated \Cpp, in a text format similar to Cabs.
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 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 0 if there are some non-fatal errors but \lstinline|--no-exit-code| is enabled (the default)
\item 1 if there are some non-fatal errors but \lstinline|--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 \lstinline|-Werror| option causes warnings to be treated as errors.
All output is sent to the standard output.\footnote{Currently clang output goes to std err.}
......@@ -243,83 +314,63 @@ All output is sent to the standard output.\footnote{Currently clang output goes
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 \\
\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-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.
\item \option{-{-}stop-annot-error} -- if set, then parsing stops on the first error; default is off
\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 for non-fatal errors.
\item \option{-{-}annot} -- enables processing \acslpp annotations (enabled by default)
\item \option{-{-}no-annot} -- disables processing \acslpp annotations
\item \lstinline|-h| -- print help information
\item \lstinline|-help| -- print more help information
\item \lstinline|-{-}version| -- print version information
\item \lstinline|-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 \lstinline|-v| -- verbose output
\item \lstinline|-{-}stop-annot-error| -- if set, then parsing stops on the first error; default is off
\end{itemize}
\section{Clang options}
Frama-Clang is built on the \clang \cpp parser.
Frama-Clang is built on the \clang \Cpp parser.
As such, the \irg executable accepts the clang
compiler options and passes them on to clang. There are many of these.
Many of these are irrelevant to \fcl as they relate to
code generation, whereas \fcl only uses \clang for parsing, name
Many of these are irrelevant to \framaclang as they relate to
code generation, whereas \framaclang only uses \clang for parsing, name
and type resolution, and producing the AST.
You can see a list of options by running
\lstinline|framaCIRGen -help|
The most significant \cl options are these:
The most significant \clang 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
\item \lstinline|-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 \lstinline|-w| -- suppress clang warnings
\item \lstinline|-Werror| -- treat warnings as errors
\end{itemize}
Although \clang can process languages other than \cpp, \cpp is the only one usable with \fclang.
Although \clang can process languages other than \Cpp, \Cpp is the only one usable with \framaclang.
\section{Default command-line}
The launching of \irg by \framac includes the following options by default. The \fc option \lstinline|-fclang-msg-key=clang| will show (among other information) the internal command-line being invoked.
The launching of \irg by \FramaC includes the following options by default. The FramaCoption \lstinline|-fclang-msg-key=clang| will show (among other information) the internal command-line being invoked.
\begin{itemize}
\item \verb|-target <target>| with the target being set according to the \lstinline|-machdep| and \lstinline|-target| options given to \framac (cf. \S\ref{sec:bit})
\item \verb|-D__FC_MACHDEP_86_32| -- also set according to the chosen architecture
\item \verb|-target <target>| with the target being set according to
the \lstinline|-machdep| and \lstinline|-target| options given to
\FramaC (cf. \S\ref{sec:bit})
\item \verb|-D__FC_MACHDEP_86_32| -- also set according to the chosen
architecture. The corresponding \verb|__FC_MACHDEP_*| macro is used in
\FramaC- and \framaclang provided standard headers for architecture-specific
features.
\item \verb|-std=c++11| -- target C++11 features
\item \verb|-nostdinc| -- use \fcl and \framac system header files, and not the compiler's own header files
\item \verb|-I$FRAMAC_SHARE/frama-clangs/libc++ -I$FRAMAC_SHARE/libc| -- include the \fclang and \framac header files, which contain system library definitions with \acslpp annotations (the paths used are controlled by the \fc options \lstinline|-cxx-c++stdlib-path| and \lstinline|-cxx-cstdlib-path|).
\item \verb|--annot| or \verb|--no-annot| according to the \verb|-annot| or \verb|-no-annot| \framac kernel option
\item \verb|-stop-annot-error| if the corresponding option (\lstinline|-fclang-warn-key=annot-error=abort|) is given to \framac
\item options to set the level of info messages and warning messages, based on options on the \fc command-line
\item \verb|-nostdinc| -- use \framaclang and \FramaC system header files, and not the compiler's own header files
\item \verb|-I$FRAMAC_SHARE/frama-clangs/libc++ -I$FRAMAC_SHARE/libc| -- include the \framaclang and \FramaC header files, which contain system library definitions with \acslpp annotations (the paths used are controlled by the FramaCoptions \lstinline|-cxx-c++stdlib-path| and \lstinline|-cxx-cstdlib-path|).
\item \verb|--annot| or \verb|--no-annot| according to the \verb|-annot| or \verb|-no-annot| \FramaC kernel option
\item \verb|-stop-annot-error| if the corresponding option (\lstinline|-fclang-warn-key=annot-error=abort|) is given to \FramaC
\item options to set the level of info messages and warning messages,
based on options on the \FramaC command-line
\end{itemize}
%\section{Custom ASTs}
%\lstset{keepspaces=true}
%In standard mode, \framac invokes \irg on a file, producing an AST in intermediate format, and the reads that intermediate file into \framac to complete the processing.
%In standard mode, \FramaC invokes \irg on a file, producing an AST in intermediate format, and the reads that intermediate file into \FramaC to complete the processing.
%If some manipulation of the AST intermediate is needed, those two steps can be performed separately as follows:
%\begin{itemize}
%\item Produce an intermediate AST \lstinline|f.ast| for a given input file \lstinline|f.cpp| using the command \\
%\centerline{\lstinline|framaCIRGen <options> -o f.ast f.cpp|}
%\item Manipulate \lstinline|f.ast| as desired.
%\item Run \framac on the AST using the command \\
%\item Run \FramaC on the AST using the command \\
%\centerline{\lstinline|frama-c <options> -cpp-command "cat f.ast" f.cpp|}
%\end{itemize}
%
......
doc/userman/eu-flag.jpg 0 → 100644
View file @ 54b2bdf8
doc/userman/eu-flag.jpg

8.18 KiB

doc/userman/fclangversion.tex
View file @ 54b2bdf8
\newcommand{\version}{0.0.7\xspace}
\newcommand{\fclangversion}{0.0.7\xspace}
\newcommand{\fcversion}{19.0~Potassium\xspace}
\newcommand{\clangversion}{6.0-8.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/frama-c-book.cls
View file @ 54b2bdf8
% --------------------------------------------------------------------------
% --- LaTeX Class for Frama-C Books ---
% --------------------------------------------------------------------------
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{frama-c-book}[2009/02/05 LaTeX Class for Frama-C Books]
% --------------------------------------------------------------------------
% --- Base Class management ---
% --------------------------------------------------------------------------
\LoadClass[a4paper,11pt,twoside,openright]{report}
\DeclareOption{web}{\PassOptionsToPackage{colorlinks,urlcolor=blue}{hyperref}}
\DeclareOption{paper}{\PassOptionsToPackage{pdfborder=0 0 0}{hyperref}}
\ProcessOptions
\RequirePackage{fullpage}
\RequirePackage{hevea}
\RequirePackage{ifthen}
\ProvidesClass{frama-c-book}
\LoadClass[a4paper]{report}
\RequirePackage{kvoptions}
\SetupKeyvalOptions{
family=framacbook,
prefix=framacbook@,
}
\DeclareStringOption[english]{lang}
\ProcessKeyvalOptions*
\PassOptionsToPackage{\framacbook@lang}{babel}
\RequirePackage{babel}
\RequirePackage[
left=.125\paperwidth,
right=.125\paperwidth,
top=.125\paperheight,
bottom=.125\paperheight
]{geometry}
\RequirePackage[dvipsnames,table]{xcolor}
\RequirePackage{graphicx}
\RequirePackage{xspace}
\RequirePackage{anyfontsize}
\RequirePackage{titletoc}
\RequirePackage{titlesec}
\RequirePackage[shortlabels]{enumitem}
\RequirePackage{fancyhdr}
\RequirePackage{lmodern}
\RequirePackage{microtype}
\RequirePackage{etoolbox}
\RequirePackage{tikz}
\usetikzlibrary{fadings}
% Do I keep it there:
\RequirePackage[T1]{fontenc}
\RequirePackage[utf8]{inputenc}
\RequirePackage[a4paper,pdftex,pdfstartview=FitH]{hyperref}
\RequirePackage{amssymb}
\RequirePackage{xcolor}
\RequirePackage[pdftex]{graphicx}
\RequirePackage{xspace}
\RequirePackage{makeidx}
\RequirePackage[leftbars]{changebar}
\RequirePackage[english]{babel}
\RequirePackage{fancyhdr}
\RequirePackage{titlesec}
\RequirePackage{comment}
\definecolor{frama-c-orange}{HTML}{F36521}
\definecolor{frama-c-dark-orange}{HTML}{D04604}
\definecolor{frama-c-dark-red}{HTML}{D00404}
\definecolor{frama-c-bronze}{HTML}{F39D21}
\definecolor{frama-c-green}{HTML}{16A371}
\definecolor{frama-c-dark-green}{HTML}{0E6647}
\RequirePackage[
pdftex,pdfstartview=FitH,
bookmarks=true,
hyperindex=true,
bookmarksopen=true,
bookmarksnumbered=true,
colorlinks=true,
allcolors={frama-c-dark-orange}
]{hyperref}
% --------------------------------------------------------------------------
% --- Page Layout ---
% CEA commands
% --------------------------------------------------------------------------
\setlength{\voffset}{-6mm}
\setlength{\headsep}{8mm}
\setlength{\footskip}{21mm}
\setlength{\textheight}{238mm}
\setlength{\topmargin}{0mm}
\setlength{\textwidth}{155mm}
\setlength{\oddsidemargin}{2mm}
\setlength{\evensidemargin}{-2mm}
\setlength{\changebarsep}{0.5cm}
\setlength{\headheight}{13.6pt}
\def\put@bg(#1,#2,#3)#4{\setlength\unitlength{1cm}%
\begin{picture}(0,0)(#1,#2)
\put(0,0){\includegraphics[width=#3cm]{#4}}
\end{picture}}
\fancypagestyle{plain}{%
\fancyfoot{}
\fancyhead{}
\fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
\fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
\fancyhead[CE]{\scriptsize\textsf{\leftmark}}
\fancyhead[CO]{\scriptsize\textsf{\rightmark}}
\fancyfoot[C]{\small\textsf{\thepage}}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\newcommand{\cealist}{CEA-List}
\newcommand
{\fcaffiliationen}
{\cealist, Université Paris-Saclay\\ Software Safety and Security Lab\xspace}
\newcommand
{\fcaffiliationfr}
{\cealist, Université Paris-Saclay\\ Laboratoire de Sûreté et Sécurité des Logiciels\xspace}
\newcommand{\cealogo}{logos/cea_tech_list.png}
% --------------------------------------------------------------------------
% LICENSE commands
% --------------------------------------------------------------------------
\def\@licence{}
\def\@licencelogo{}
\def\@licencelink{}
\newcommand{\licence}[3]{
\def\@licence{#1}
\def\@licencelogo{#2}
\def\@licencelink{#3}
}
\fancypagestyle{blank}{%
\fancyfoot{}
\fancyhead{}
\fancyhead[LE]{\put@bg(2.4,27.425,21){frama-c-left.pdf}}
\fancyhead[LO]{\put@bg(2.7,27.425,21){frama-c-right.pdf}}
\newcommand{\cclicence}[1]{
\licence
{Creative Commons \uppercase{#1}}
{logos/#1.png}
{\url{https://creativecommons.org/licenses/#1/4.0/}}
}
%% Redefinition of cleardoublepage for empty page being blank
\def\cleardoublepagewith#1{\clearpage\if@twoside \ifodd\c@page\else
\hbox{}
\thispagestyle{#1}
\newpage
\fi\fi}
\def\cleardoublepage{\cleardoublepagewith{blank}}
\pagestyle{plain}
% --------------------------------------------------------------------------
% --- Cover Page ---
% Copyright commands
% --------------------------------------------------------------------------
\newcommand{\coverpage}[1]{%
\thispagestyle{empty}
\setlength\unitlength{1cm}
\begin{picture}(0,0)(3.27,26.75)
\put(0.58,0.70){\includegraphics[width=20.9cm]{frama-c-cover.pdf}}
\put(2.0,20.5){\makebox[8cm][l]{\fontfamily{phv}\fontseries{m}\fontsize{24}{2}\selectfont #1}}
\end{picture}
\def\@copyrightfrom{}
\newcommand{\copyrightstarts}[1]{
\def\@copyrightfrom{#1}
}
\newcommand{\addcopyrightowner}[1]{
\listadd{\@copyrightowner}{#1}
}
\addcopyrightowner{\cealist} % add it by default
\newcommand{\insertcopyrightowners}{{
\def\listsep{\def\listsep{, }}%
\renewcommand{\do}[1]{\listsep##1}%
\dolistloop\@copyrightowner
}}
\newcommand{\insertcopyright}{
\textcopyright\xspace \@copyrightfrom-\the\year{} \insertcopyrightowners
}
% --------------------------------------------------------------------------
% Logos
% --------------------------------------------------------------------------
\def\@logos{}
\newcommand{\addlogo}[1]{
\listadd{\@logos}{#1}
}
\addlogo{\cealogo} % add it by default
\newcommand{\insertlogos}{{
\def\listsep{\def\listsep{\hspace{2em}}}%
\renewcommand{\do}[1]{\listsep\includegraphics[height=7em]{##1}}%
\dolistloop\@logos
}}
% --------------------------------------------------------------------------
% --- Title Page ---
% Subtitle
% --------------------------------------------------------------------------
\renewenvironment{titlepage}%
{\cleardoublepagewith{empty}\thispagestyle{empty}\begin{center}}%
{\end{center}}
\renewcommand{\title}[2]{
\vspace{20mm}
{\Huge\bfseries #1}
\bigskip
\def\@subtitle{}
{\LARGE #2}
\vspace{20mm}
\newcommand{\subtitle}[1]{
\def\@subtitle{#1}
}
\renewcommand{\author}[1]{
\vspace{20mm}
{#1}
% --------------------------------------------------------------------------
% Frama-C commands
% --------------------------------------------------------------------------
\medskip
\def\@fcversion{}
\newcommand{\fcversion}[1]{
\subtitle{For Frama-C #1}
}
\def\fchrulefill{\leavevmode\leaders\hrule height 1.25pt\hfill\kern\z@}
% --------------------------------------------------------------------------
% --- Sectionning ---
% Title page
% --------------------------------------------------------------------------
\titleformat{\chapter}[display]{\Huge\raggedleft}%
{\huge\chaptertitlename\,\thechapter}{0.5em}{}
\titleformat{\section}[hang]{\Large\bfseries}{\thesection}{1em}{}%
[\vspace{-14pt}\rule{\textwidth}{0.1pt}\vspace{-8pt}]
\titleformat{\subsubsection}[hang]{\bfseries}{}{}{}%
[\vspace{-8pt}]
\renewcommand{\maketitle}{%
\newgeometry{top=1cm, bottom=1cm, right=1cm,left=1cm}
\thispagestyle{empty}
\noindent\includegraphics{logos/frama-c.png}
\vspace{12em}
\begin{center}
\textbf{\Huge\@title}
\medskip
\ifx\@subtitle\empty\else{
\Large \@subtitle
}\fi
\end{center}
\vspace{-1em}
{\noindent\color{frama-c-orange}\fchrulefill}
\begin{center}
\begin{minipage}{.8\textwidth}
\centering
\large\@author
\end{minipage}
\end{center}
\bigskip
\begin{center}
\insertlogos
\end{center}
\vfill
\noindent
\ifx\@licencelogo\empty
\else{
\begin{minipage}{.14\textwidth}
\includegraphics[height=25pt]{\@licencelogo}
\end{minipage}
\hfill
}
\fi
\begin{minipage}{.84\textwidth}
\vspace{.2em}
\ifx\@licence\empty
\else{\large Work licensed under \@licence\xspace licence}\fi\\
\ifx\@licencelink\empty
\else{\large\@licencelink}\fi
\end{minipage}
\medskip
\noindent\insertcopyright
\restoregeometry%
\cleardoublepage
}
% --------------------------------------------------------------------------
% Table of contents
% --------------------------------------------------------------------------
\titlecontents{chapter}
[0em]
{\bigskip}
{\makebox[2em][l]{\thecontentslabel}\bfseries}
{\hspace*{2em}\bfseries}
{\space\hfill\makebox[1.5em]{\contentspage}}[]
\titlecontents{section}
[2em]
{\medskip}
{\makebox[3em][l]{\thecontentslabel}}
{\hspace*{3em}}
{\titlerule*[1pc]{.}\makebox[1.5em]{\contentspage}}[]
\titlecontents{subsection}
[5em]
{\smallskip}
{\makebox[4.5em][l]{\thecontentslabel}}
{\hspace*{4.5em}}
{\titlerule*[1pc]{.}\makebox[1.5em]{\contentspage}}[]
% --------------------------------------------------------------------------
% Acknoledgements
% --------------------------------------------------------------------------
\def\@people{}
\newcommand{\acknowledge}[1]{
\listadd{\@people}{#1}
}
\newcommand{\commaorandlist}[1]{%
\count255=0
\def\do##1{\advance\count255 1 \chardef\finalitem=\count255 }%
\dolistloop{#1}%
\count255=0
\def\do##1{\advance\count255 1
\ifnum\count255=\finalitem
\space and\space
\else
\ifnum\count255=1\else,\space\fi
\fi##1}
\dolistloop{#1}}
\newcommand{\insertpeople}{{
\ifx\@people\empty\else
{We gratefully thank all the people who contributed to this document: \commaorandlist\@people.}
\fi
}}
% \acknowledgeprogram{<flag image file>}{<text inside box>}
\newcommand{\acknowledgeprogram}[2]{
\noindent\fbox{%
\parbox{\dimexpr\linewidth-2\fboxsep-2\fboxrule}{%
\begin{minipage}{1.2cm}%
\includegraphics[width=\textwidth]{#1}%
\end{minipage}%
\hfill%
\begin{minipage}{0.9\textwidth}%
This project has received funding from #2.%
\end{minipage}%
}%
}%
}
\newcommand{\acknowledgeANR}[1]{
\acknowledgeprogram{anr-logo.png}{#1}
}
\newcommand{\acknowledgeEU}[1]{
\acknowledgeprogram{eu-flag.jpg}{#1}
}
% --------------------------------------------------------------------------
% Header
% --------------------------------------------------------------------------
\pagestyle{fancy}
\fancyhf{}
\fancyhead[L]{\vspace{1.25em}\raggedleft\rightmark\vspace{-1.25em}}
\fancyfoot[C]{\thepage}
\renewcommand{\headrulewidth}{0pt}
\setlength{\headheight}{24pt}
% --------------------------------------------------------------------------
% --- Main Text Style ---
% Chapters
% --------------------------------------------------------------------------
%\raggedright
\setlength\parindent{0pt}
\setlength\parskip{1ex plus 0.3ex minus 0.2ex}
\newenvironment{warning}[1][Warning:]{\small\paragraph{#1}\itshape}{\vspace{\parskip}}
\def\FramaC{\textsf{Frama-C}\xspace}
\titleformat{\chapter}[display]
{\sc\huge}
{\filleft\fontsize{50}{0}\selectfont\thechapter}
{-1.1em}
{\filright}
[\normalsize\vspace{-.5em}\color{frama-c-orange}\fchrulefill]
\titleformat{\section}[hang]
{\Large\bfseries}
{\thesection}
{1em}
{}
[\vspace{-10pt}\rule{\textwidth}{0.1pt}\nopagebreak\vspace{-8pt}]
\titlespacing*{\section}{0pt}{20pt}{20pt}
% --------------------------------------------------------------------------
% Itemize style
% --------------------------------------------------------------------------
\renewcommand\labelitemi{--}
\setitemize{noitemsep,topsep=5pt,parsep=0pt,partopsep=0pt}
\setenumerate{noitemsep,topsep=5pt,parsep=0pt,partopsep=0pt}
% --------------------------------------------------------------------------
% Footnote style
% --------------------------------------------------------------------------
% --- Listings ---
\renewcommand\footnoterule{%
\kern-3\p@%
{\color{frama-c-orange}\hrule\@width\columnwidth}%
\kern2.6\p@%
}
\renewcommand{\@makefntext}[1]{
\setlength{\parindent}{0pt}
\begin{list}{}{\setlength{\labelwidth}{1.5em}
\setlength{\leftmargin}{\labelwidth}
\setlength{\labelsep}{3pt}
\setlength{\itemsep}{0pt}
\setlength{\parsep}{0pt}
\setlength{\topsep}{3pt}
\footnotesize}
\item[\@makefnmark\hfil]#1
\end{list}
}
% --------------------------------------------------------------------------
% Warning & information style
% --------------------------------------------------------------------------
\newsavebox{\fcsavebox}
\newenvironment{colbox}[1]{%
\newcommand\colboxcolor{#1}%
\begin{lrbox}{\fcsavebox}%
\begin{minipage}{\dimexpr\linewidth-2\fboxsep\relax}
\itshape
}{%
\end{minipage}\end{lrbox}%
\begin{center}
\colorbox{\colboxcolor}{\usebox{\fcsavebox}}
\end{center}
}
\newenvironment{important}{\begin{colbox}{frama-c-dark-orange!30}}{\end{colbox}}
\newenvironment{information}{\begin{colbox}{frama-c-green!30}}{\end{colbox}}
% --------------------------------------------------------------------------
% Code
% --------------------------------------------------------------------------
\RequirePackage{scrhack} % avoids warning about \float@addtolists related to lstlisting
\RequirePackage{listings}
\RequirePackage{caption}
\RequirePackage{accsupp}
\lstdefinelanguage{ACSL}{%
morekeywords={allocates,assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
exit_behavior,frees,ghost,global,inductive,integer,invariant,lemma,logic,loop,
model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
union,variant},
keywordsprefix={\\},
alsoletter={\\},
morecomment=[l]{//}
\newcommand{\noncopynumber}[1]{%
\BeginAccSupp{method=escape,ActualText={}}%
#1%
\EndAccSupp{}%
}
\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
\definecolor{lstbg}{gray}{0.98}
\definecolor{lstfg}{gray}{0.10}
\definecolor{lstrule}{gray}{0.6}
\definecolor{lstnum}{gray}{0.4}
\renewcommand{\ttdefault}{pcr} % so that keywords can be bold
% CAPTION
\DeclareCaptionFormat{listing}{
\raggedright\textbf{#1 #2} #3
\vspace{-2mm}
{\color{gray}\rule{\textwidth}{0.1pt}}
}
\DeclareCaptionLabelSeparator{listing}{--}
\captionsetup[lstlisting]{format=listing,labelsep=listing}
% Basic style
% --------------------------------------------------------------------------
\definecolor{lstnum}{gray}{0.3}
\definecolor{lsttxt}{rgb}{0.3,0.2,0.6}
\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}%{0.6,0.6,0.2}
\definecolor{lstmodule}{rgb}{0.3,0.6,0.2}
\definecolor{lstspecial}{rgb}{0.2,0.6,0.0}
\definecolor{lstfile}{gray}{0.85}
\definecolor{lstcomments}{rgb}{0.35,0.35,0.35}
\newcommand{\lstbrk}{\mbox{$\color{blue}\scriptstyle\cdots$}}
\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\scriptsize\else\normalfont\ttfamily\mdseries\scriptsize\fi}
\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\small\fi}
\def\lp@basic{\ifmmode\normalfont\mathtt\mdseries\small\else\normalfont\ttfamily\mdseries\small\fi}
\def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\normalsize\fi}
\def\lp@keyword{}
\def\lp@special{\color{lstfg}}
\def\lp@comment{\normalfont\ttfamily\mdseries}
\def\lp@string{\color{lstfg}} \def\lp@ident{}
\def\lp@number{\rmfamily\tiny\color{lstnum}}
\lstdefinestyle{frama-c-style}{%
\def\lp@special{\color{frama-c-dark-orange}}
\def\lp@comment{\normalfont\ttfamily\mdseries\color{lstcomments}}
\def\lp@string{\color{frama-c-dark-green}}
\def\lp@ident{}
\def\lp@number{\rmfamily\tiny\color{lstnum}\noncopynumber}
\lstdefinestyle{frama-c-basic-style}{%
captionpos=b,%
columns=flexible,%
basicstyle=\lp@inline,%
identifierstyle=\lp@ident,%
commentstyle=\lp@comment,%
keywordstyle={\ifmmode\mathsf\else\sffamily\fi},%
keywordstyle=[2]\lp@special,%
keywordstyle={\bfseries\ifmmode\mathsf\else\ttfamily\fi\color{blue}},%
keywordstyle=[2]\bfseries\lp@special,%
stringstyle=\lp@string,%
emphstyle=\lp@ident\underbar,%
showstringspaces=false,%
mathescape=true,%
numberstyle=\lp@number,%
xleftmargin=6ex,xrightmargin=2ex,%
xleftmargin=1.82em,%
framexleftmargin=1ex,%
frame=l,%
framerule=1pt,%
rulecolor=\color{lstrule},%
backgroundcolor=\color{lstbg},%
rulecolor=\color{frama-c-orange!60},%
backgroundcolor=\color{frama-c-bronze!10},%
literate={\ }{\ }1,
% ^~~~~ Without this, spaces starting a line does not have the right size ...
}
\lstdefinestyle{frama-c-style}{%
style=frama-c-basic-style,%
moredelim={*[s]{/*@}{*/}},%
moredelim={*[l]{//@}},%
morecomment={[il]{//NOPP-LINE}},% invisible comment until end of line
morecomment={[is]{//NOPP-BEGIN}{NOPP-END\^^M}},% no space after NOPP-END
mathescape=true,
escapechar=`
% breaklines is broken when using a inline and background
% breaklines,prebreak={\lstbrk},postbreak={\lstbrk},breakindent=5ex %
}
% Code styles
% --------------------------------------------------------------------------
\lstdefinestyle{frama-c-shell-style}{%
mathescape=false,%
basicstyle=\lp@basic,%
keywordstyle=\sffamily\bfseries,%
keywordstyle=[1]\sffamily\color{lstmodule},%
keywordstyle=[2]\sffamily\color{lstspecial},%
keywordstyle=[3]\sffamily\bfseries,%
identifierstyle=\ttfamily,%
stringstyle=\ttfamily\color{frama-c-orange},%
commentstyle=\rmfamily\bfseries\color{lsttxt},%
literate={\\\$}{\$}1%
{€}{\textbackslash}1%
,%
}
% ACSL + C
% --------------------------------------------------------------------------
\lstdefinelanguage{ACSL}{%
escapechar={},
literate=,
breaklines=false,
classoffset=1,
morekeywords={admit,allocates,assert,assigns,assumes,axiom,axiomatic,behavior,
behaviors,boolean,breaks,calls,check,complete,continues,data,decreases,disjoint,
ensures,exits,frees,ghost,global,import,inductive,integer,invariant,lemma,
logic,loop,model,module,predicate,reads,real,requires,sizeof,strong,struct,
terminates,returns,type,union,variant,
dynamic_split,merge,pragma,slevel,split,taints,taint,unroll,widen_hints,
\\tainted,
Here,LoopCurrent,LoopEntry,Pre,Post,Old,
\\Cons,\\Down,\\NearestAway,\\NearestEven,\\Nil,\\ToZero,\\Up,
\\as,\\at,\\allocable,\\allocation,\\automatic,\\base_addr,\\block_length,\\dangling,
\\dynamic,\\exists,\\exit_status,\\false,\\forall,\\freeable,\\fresh,\\from,
\\in,\\initialized,\\lambda,\\let,\\list,\\match,\\nothing,\\null,\\numof,
\\object_pointer,\\offset,\\old,\\register,\\result,\\separated,\\static,
\\sum,\\true,\\unallocated,\\valid,\\valid_function,\\valid_read,\\object_pointer,\\with},
classoffset=0,
alsoletter={\\},
morecomment=[l]{//}
}
\lstloadlanguages{[ANSI]C,[Objective]Caml,csh,ACSL}
\lstdefinestyle{c}%
{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style}
\lstdefinestyle{c-basic}%
{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
% --- C/ACSL Stuff ---------------------------------------------------------
% Make 'c' the default style
\lstset{style=c}
\newcommand{\listinginput}[3][1]%
{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2]{#3}}
\newcommand{\listinginputcaption}[4][1]%
{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,title=#3]{#4}}
{\lstinputlisting[style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2,caption={#3}]{#4}}
\lstnewenvironment{listing}[2][1]%
{\lstset{style=c-basic,numbers=left,stepnumber=#1,firstnumber=#2}}{}
\lstnewenvironment{listing-nonumber}%
{\lstset{style=c,numbers=none,basicstyle=\lp@basic}}{}
% --- Verbatim Stuff -------------------------------------------------------
\lstdefinelanguage{Shell}[]{csh}%
{identifierstyle=\lp@basic,mathescape=false,backgroundcolor=,literate={\\\$}{\$}1}
\lstnewenvironment{shell}[1][]{\lstset{language=Shell,basicstyle=\lp@basic,#1}}{}
% Commands used mainly by Eva manual
% ---- Stdout Stuff --------------------------------------------------------
\lstdefinelanguage{Logs}[]{csh}%
{identifierstyle=\lp@basic,backgroundcolor=}
\lstnewenvironment{logs}[1][]{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
\newcommand{\logsinput}[1]%
{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}
\newcommand{\logwithrange}[2]%
{\lstinputlisting[breaklines=true,basicstyle=\ttfamily\small,linerange=#1]{#2}}
\newcommand{\cwithrange}[2]%
{\lstinputlisting[style=c-basic,numbers=left,linerange=#1]{#2}}
\newcommand{\csource}[1]%
{\lstinputlisting[style=c-basic,numbers=left]{#1}}
\lstnewenvironment{listing-log}%
{\lstset{numbers=none,basicstyle=\lp@basic}}{}
% ACSL + C (developers)
% --------------------------------------------------------------------------
% --- Developer Code Stuff ---
% --------------------------------------------------------------------------
\newcommand{\listingname}[1]{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
% --- Style ----------------------------------------------------------------
\lstdefinestyle{framac-code-style}{%
basicstyle=\lp@inline,%
numberstyle=\lp@number,%
keywordstyle=[1]\sffamily\color{lstmodule},%
keywordstyle=[2]\sffamily\color{lstspecial},%
keywordstyle=[3]\sffamily\bfseries,%
identifierstyle=\rmfamily,%
stringstyle=\ttfamily\color{lstfg},%
commentstyle=\rmfamily\bfseries\color{lsttxt},%
}
\lstdefinestyle{framac-shell-style}{%
mathescape=false,%
basicstyle=\lp@basic,%
numberstyle=\lp@number,%
keywordstyle=\sffamily\bfseries,%
keywordstyle=[1]\sffamily\color{lstmodule},%
keywordstyle=[2]\sffamily\color{lstspecial},%
keywordstyle=[3]\sffamily\bfseries,%
identifierstyle=\ttfamily,%
stringstyle=\ttfamily\color{lstfg},%
commentstyle=\rmfamily\bfseries\color{lsttxt},%
literate={\\\$}{\$}1,%
}
% --- Configure ------------------------------------------------------------
\lstdefinestyle{framac-code}%
{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic}
\newcommand{\cinput}[2][]%
{\lstinputlisting[
language={[ANSI]C},
alsolanguage=ACSL,
style=frama-c-style,#1]{#2}
}
\newcommand{\cinline}[1]%
{\lstinline[style=framac-code]{#1}}
\lstnewenvironment{ccode}[1][]%
{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=frama-c-style,basicstyle=\lp@basic,#1}}{}
% Configure
% --------------------------------------------------------------------------
\lstdefinelanguage{Configure}[]{csh}{%
style=framac-shell-style,%
morekeywords={fi},%
style=frama-c-shell-style,%
morekeywords={fi},%
}
\newcommand{\configureinput}[1]%
{\lstinputlisting[language=Configure]{#1}}
\lstnewenvironment{configurecode}[1][]%
{\lstset{language=Configure,#1}}{}
\newcommand{\configureinput}[1]{\lstinputlisting[language=Configure]{#1}}
% --- Makefile ------------------------------------------------------------
% Commands
% --------------------------------------------------------------------------
\lstdefinelanguage{frama-c-commands}[]{}{%
mathescape=false,%
alsoletter=-.,%
keywordstyle=\color{frama-c-green}\bfseries,%
keywordstyle=[2]\color{frama-c-dark-red}\bfseries,%
classoffset=0,%
keywords={e-acsl-gcc.sh,frama-c,frama-c-gui,frama-c-script},%
classoffset=1,%
morekeywords={-load,-then,-then-last,-then-on,-then-replace,-save},%
classoffset=0,%
morestring=[b]{'},
morestring=[b]{"},
literate={\\\$}{\$}1%
}
\lstnewenvironment{frama-c-commands}[1][]
{\lstset{style=frama-c-basic-style,language=frama-c-commands,#1}}{}
% Dune
% --------------------------------------------------------------------------
\lstdefinelanguage{Dune}{%
literate=%
{à}{{\`a}}1%
{é}{{\'e}}1%
,
style=frama-c-style,%
alsoletter=:-,%
keywords={%
action,alias,as,backend,context,default,deps,dune,executable,%
env,env-vars,files,flags,from,generate_opam_files,install,%
instrument_with,instrumentation,lang,libraries,library,name,optional,%
package,plugin,profile,progn,public_name,rule,section,select,site,%
targets,using%
},%
morekeywords=[2]{%
:standard%
},%
morecomment=[l]{;},%
}
\lstdefinestyle{dune-basic}{%
language=Dune,%
style=frama-c-basic-style,%
basicstyle=\lp@inline,%
}
\newcommand{\duneinput}[2][]{\lstinputlisting[style=dune-basic,#1]{#2}}
\lstnewenvironment{dunecode}[1][]{\lstset{style=dune-basic,#1}}{}
% Logs
% --------------------------------------------------------------------------
\lstdefinelanguage{Logs}[]{}{%
style=frama-c-basic-style,
mathescape=false,
backgroundcolor=,
literate={\\\$}{\$}1
}
\newcommand{\logsinput}[1]%
{\lstinputlisting[language=Logs,basicstyle=\lp@basic]{#1}}
\lstnewenvironment{logs}[1][]%
{\lstset{language=Logs,basicstyle=\lp@basic,#1}}{}
% Makefile
% --------------------------------------------------------------------------
\lstdefinelanguage{Makefile}[]{make}{%
style=framac-shell-style,%
morekeywords={include},%
style=frama-c-shell-style,%
morekeywords={include},%
}
\lstdefinestyle{make-basic}{%
language=Makefile,%
style=frama-c-basic-style,%
basicstyle=\lp@inline,%
}
\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
\newcommand{\makeinput}[2][]{\lstinputlisting[style=make-basic,#1]{#2}}
\lstnewenvironment{makefilecode}[1][]%
{\lstset{language=Makefile,#1}}{}
\newcommand{\makefileinput}[1]{\lstinputlisting[language=Makefile]{#1}}
% --- C- for Developer ----------------------------------------------------
\lstdefinestyle{framac-code}%
{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
\lstnewenvironment{ccode}[1][]%
{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
\newcommand{\cinput}[1]%
{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic]{#1}}
\newcommand{\cinline}[1]%
{\lstinline[style=framac-code]{#1}}
% --- Ocaml ----------------------------------------------------------------
\lstnewenvironment{makecode}[1][]%
{\lstset{style=make-basic,#1}}{}
% OCaml
% --------------------------------------------------------------------------
\lstdefinelanguage{Ocaml}[Objective]{Caml}{%
style=framac-code-style,%
deletekeywords={when,module,struct,sig,begin,end},%
morekeywords=[2]{failwith,raise,when},%
morekeywords=[3]{module,struct,sig,begin,end},%
literate=%
{~}{${\scriptstyle\thicksim}$}1%
{<}{$<$}1%
{>}{$>$}1%
{->}{$\rightarrow$}1%
{<-}{$\leftarrow$}1%
{:=}{$\leftarrow$}1%
{<=}{$\leq$}1%
{>=}{$\geq$}1%
{==}{$\equiv$}1%
{!=}{$\not\equiv$}1%
{<>}{$\neq$}1%
{'a}{$\alpha$}1%
{'b}{$\beta$}1%
{'c}{$\gamma$}1%
{}{`{}}1%
}
\lstdefinestyle{ocaml-basic}%
{language=Ocaml,basicstyle=\lp@basic}
style=frama-c-basic-style,%
deletekeywords={when,module,struct,sig,begin,end},%
morekeywords=[2]{failwith,raise,when},%
morekeywords=[3]{module,struct,sig,begin,end},%
literate=%
{~}{${\scriptstyle\thicksim}$}1%
{<}{$<$ }1%
{>}{$>$ }1%
{->}{$\rightarrow$ }1%
{<-}{$\leftarrow$ }1%
{:=}{$\leftarrow$ }1%
{<=}{$\leq$ }1%
{>=}{$\geq$ }1%
{==}{$\equiv$ }1%
{!=}{$\not\equiv$ }1%
{<>}{$\neq$ }1%
{'a}{$\alpha$ }1%
{'b}{$\beta$ }1%
{'c}{$\gamma$ }1%
{µ}{`{}}1%
{€}{\textbackslash}1%
{à}{{\`a}}1%
{é}{{\'e}}1%
}
\lstdefinestyle{ocaml-basic}{
language=Ocaml,
basicstyle=\lp@basic
}
\newcommand{\ocamlinput}[2][]{\lstinputlisting[style=ocaml-basic,#1]{#2}}
\lstnewenvironment{ocamlcode}[1][]{\lstset{style=ocaml-basic,#1}}{}
% Shell
% --------------------------------------------------------------------------
\lstdefinelanguage{Shell}[]{csh}{%
escapechar=@
identifierstyle=\lp@basic,
mathescape=false,
backgroundcolor=,
literate={\\\$}{\$}1
}
\newcommand{\listingname}[1]%
{\colorbox{lstfile}{\footnotesize\sffamily File \bfseries #1}\vspace{-4pt}}
\lstnewenvironment{shell}[1][]
{\lstset{language=Shell,basicstyle=\lp@basic,#1}}{}
% Why
% --------------------------------------------------------------------------
\lstdefinelanguage{Why}{%
morekeywords={
type, logic, axiom, predicate, goal,
......@@ -311,22 +727,22 @@ literate=%
{not}{$\neg$}1%
{<>}{$\neq$}1%
{...}{$\dots$}1%
%{_}{\_}1%
%{_}{{\rule[0pt]{1ex}{.2pt}}}1%
}
}
\lstdefinestyle{why-style}{%
language=Why,%
style=framac-code-style,%
basicstyle=\lp@inline,%
language=Why,%
style=frama-c-basic-style,%
basicstyle=\lp@inline,%
}
\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
\newcommand{\whyinput}[1]%
{\lstinputlisting[style=why-style,basicstyle=\lp@basic]{#1}}
\newcommand{\whyinline}[1]%
{\lstinline[style=why-style]{#1}}
\lstnewenvironment{whycode}[1][]{\lstset{style=why-style,#1}}{}
% Default style is empty
% --------------------------------------------------------------------------
% --- End. ---
% --------------------------------------------------------------------------
\lstset{style=frama-c-style}
doc/userman/frama-c-cover.pdf deleted 100644 → 0
View file @ 76190d5c
File deleted
doc/userman/frama-c-left.pdf deleted 100644 → 0
View file @ 76190d5c
File deleted
doc/userman/frama-c-right.pdf deleted 100644 → 0
View file @ 76190d5c
File deleted
doc/userman/grammar.tex
View file @ 54b2bdf8
\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
View file @ 54b2bdf8
\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
View file @ 54b2bdf8
\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}
......@@ -15,6 +15,8 @@ The following C++ features are not implemented in \acslpp.
\item uses of typename
\item uses of templates are not robust
\item uses of typeid
\item implementation of the standard library is very rudimentary
\item main target of \framaclang is C++11
\end{itemize}
\section{Implementation of \acslpp}
......@@ -22,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 *
......
doc/userman/logos/by-nc-nd.eu.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/by-nc-nd.eu.png

10.4 KiB

doc/userman/logos/by-nc-nd.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/by-nc-nd.png

20.4 KiB

doc/userman/logos/by-nc-sa.eu.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/by-nc-sa.eu.png

11 KiB

doc/userman/logos/by-nc-sa.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/by-nc-sa.png

21.9 KiB

doc/userman/logos/by-nc.eu.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/by-nc.eu.png

9.1 KiB

doc/userman/logos/by-nc.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/by-nc.png

17.2 KiB

doc/userman/logos/by-nd.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/by-nd.png

15.8 KiB

doc/userman/logos/by-sa.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/by-sa.png

17.2 KiB

doc/userman/logos/by.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/by.png

12.3 KiB

doc/userman/logos/cc-zero.png 0 → 100644
View file @ 54b2bdf8
doc/userman/logos/cc-zero.png

6.3 KiB