Skip to content
Snippets Groups Projects
Commit 3f8b93e3 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[doc] fix RTE overfull hbox

parent af0eec33
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 51 additions and 82 deletions
doc/rte/rte.tex
+ 51
− 82
View file @ 3f8b93e3
...@@ -204,11 +204,12 @@ complement, the interval of representable values also corresponds to $[-2^{n-1}, ...@@ -204,11 +204,12 @@ complement, the interval of representable values also corresponds to $[-2^{n-1},
included, but not the padding bits if there are any). The size in bits of a included, but not the padding bits if there are any). The size in bits of a
type is obtained through \lstinline|Cil.bitsSizeOf: typ -> int|, which bases type is obtained through \lstinline|Cil.bitsSizeOf: typ -> int|, which bases
itself on the machine dependency option of Frama-C. For instance by using itself on the machine dependency option of Frama-C. For instance by using
\lstinline|-machdep x86_32|, we have the following: \lstinline|-machdep x86_32|, we have the following (the size is expressed in
bits):
\begin{center} \begin{center}
\begin{tabular}{|l|c|l|} \begin{tabular}{|l|c|l|}
\hline \hline
type & size in bits & representable interval \\ type & size & representable interval \\
\hline \hline
\lstinline|signed char| & 8 & \lstinline|[-128,127]| \\ \lstinline|signed char| & 8 & \lstinline|[-128,127]| \\
\lstinline|signed short| & 16 & \lstinline|[-32768,32767]| \\ \lstinline|signed short| & 16 & \lstinline|[-32768,32767]| \\
...@@ -220,7 +221,6 @@ type & size in bits & representable interval \\ ...@@ -220,7 +221,6 @@ type & size in bits & representable interval \\
%%\caption{Signed integer types: bit sizes and interval of values} %%\caption{Signed integer types: bit sizes and interval of values}
\end{center} \end{center}
\medskip \medskip
Frama-C annotations added by plug-ins such as \rte{} may not contain macros Frama-C annotations added by plug-ins such as \rte{} may not contain macros
since pre-processing is supposed to take place beforehand (user annotations at since pre-processing is supposed to take place beforehand (user annotations at
...@@ -830,7 +830,53 @@ of Frama-C. The plug-in then selects every C function which is in the set ...@@ -830,7 +830,53 @@ of Frama-C. The plug-in then selects every C function which is in the set
defined by the \lstinline|-rte-select|: if no explicit set of functions is defined by the \lstinline|-rte-select|: if no explicit set of functions is
provided by the user, all C functions defined in the program are selected. provided by the user, all C functions defined in the program are selected.
Selecting the kind of annotations which will be generated is performed by using Selecting the kind of annotations which will be generated is performed by using
other \rte{} options (see fig.~\ref{kernel} and~\ref{options} for a summary). other \rte{} options:
\begin{description}
\item[{\tt -rte} (boolean, defaults to false)] \ \smallskip \\
Enable \rte{} plug-in
\item[{\tt -rte-div} (boolean, defaults to true)] \ \smallskip \\
Generate annotations for division by zero
\item[{\tt -rte-float-to-int} (boolean (defaults to true))] \ \smallskip \\
Generate annotations for casts from floating-point to integer
\item[{\tt -rte-initialized} (set of function (defaults to none))] \ \smallskip \\
Generate annotations for initialization for the given set of functions
\item[{\tt -rte-mem} (boolean (defaults to true))] \ \smallskip \\
Generate annotations for validity of left-values access
\item[{\tt -rte-pointer-call} (boolean (defaults to true))] \ \smallskip \\
Generate annotations for validity of calls via function pointers
\item[{\tt -rte-shift} (boolean (defaults to true))] \ \smallskip \\
Generate annotations for left and right shift value out of bounds
\item[{\tt -rte-select} (set of function (defaults to all))] \ \smallskip \\
Run plug-in on a subset of C functions
\item[{\tt -rte-trivial-annotations} (boolean (defaults to false))] \ \smallskip \\
Generate all annotations even when they trivially hold
\item[{\tt -rte-warn} (boolean (defaults to true))] \ \smallskip \\
Emit warning on broken annotations
\end{description}
Combined with the following Kernel options:
\begin{description}
\item[{\tt -warn-unsigned-overflow} (boolean, defaults to false)] \ \smallskip \\
Generate annotations for unsigned overflows
\item[{\tt -warn-unsigned-downcast} (boolean, defaults to false)] \ \smallskip \\
Generate annotations for unsigned integer downcast
\item[{\tt -warn-signed-overflow} (boolean, defaults to true)] \ \smallskip \\
Generate annotations for signed overflows
\item[{\tt -warn-signed-downcast} (boolean, defaults to false)] \ \smallskip \\
Generate annotations for signed integer downcast
\item[{\tt -warn-pointer-downcast} (boolean, defaults to true)] \ \smallskip \\
Generate annotations for downcast of pointer values
\item[{\tt -warn-left-shift-negative} (boolean, defaults to true)] \ \smallskip \\
Generate annotations for left shift on negative values
\item[{\tt -warn-right-shift-negative} (boolean, defaults to false)] \ \smallskip \\
Generate annotations for right shift on negative values
\item[{\tt -warn-invalid-bool} (boolean, defaults to true)] \ \smallskip \\
Generate annotations for \lstinline|_Bool| trap representations
\item[{\tt -warn-special-float} (string: {\tt non-finite} (default), {\tt nan} or {\tt none})] \ \smallskip \\
Generate annotations when special floats are produced: infinite floats or
NaN (by default), only on NaN or never.
\item[{\tt -warn-invalid-pointer} (boolean, defaults to false)] \ \smallskip \\
Generate annotations for invalid pointer arithmetic
\end{description}
Pretty-printing the output of \rte{} and relaunching the plug-in on the Pretty-printing the output of \rte{} and relaunching the plug-in on the
resulting file will generate duplicated annotations, since the plug-in does not resulting file will generate duplicated annotations, since the plug-in does not
...@@ -838,85 +884,8 @@ check existing annotations before generation. This behaviour does not happen if ...@@ -838,85 +884,8 @@ check existing annotations before generation. This behaviour does not happen if
\rte{} is used in the context of a Frama-C project~\cite{framacdev}: the \rte{} is used in the context of a Frama-C project~\cite{framacdev}: the
annotations are not generated twice. annotations are not generated twice.
\begin{table}
\begin{center}
\begin{tabular}{|l|l|p{4.5cm}|}
\hline
{\bf Option} & {\bf Type (Default)} & {\bf Description} \\
\hline
\lstinline|-warn-unsigned-overflow| & boolean (false) & Generate annotations for
unsigned overflows\\
\hline
\lstinline|-warn-unsigned-downcast| & boolean (false) & Generate annotations for
unsigned integer downcast\\
\hline
\lstinline|-warn-signed-overflow| & boolean (true) & Generate annotations for
signed overflows \\
\hline
\lstinline|-warn-signed-downcast| & boolean (false) & Generate annotations for
signed integer downcast \\
\hline
\lstinline|-warn-pointer-downcast| & boolean (true) & Generate annotations for
downcast of pointer values \\
\hline
\lstinline|-warn-left-shift-negative| & boolean (true) & Generate annotations for
left shift on negative values \\
\hline
\lstinline|-warn-right-shift-negative| & boolean (false) & Generate annotations for
right shift on negative values \\
\hline
\lstinline|-warn-invalid-bool| & boolean (true) & Generate annotations for
\lstinline|_Bool| trap representations \\
\hline
\lstinline|-warn-special-float| & string: (\lstinline|non-finite|), \lstinline|nan| or \lstinline|none| & generate annotations when
special floats are produced: infinite floats or NaN (by default), only on NaN or never. \\
\hline
\lstinline|-warn-invalid-pointer| & boolean (false) & Generate annotations for
invalid pointer arithmetic \\
\hline
\end{tabular}
\caption{\framac kernel options, impacting \rte{}} \label{kernel}
\end{center}
\end{table}
\begin{table}
\begin{center}
\begin{tabular}{|l|l|p{7cm}|}
\hline
{\bf Option} & {\bf Type (Default)} & {\bf Description} \\
\hline
\lstinline|-rte| & boolean (false) & Enable \rte{} plug-in \\
\hline
\lstinline|-rte-div| & boolean (true) & Generate annotations for division by
zero \\
\hline
\lstinline |-rte-float-to-int| & boolean (true) & Generate annotations for
casts from floating-point to integer \\
\hline
\lstinline |-rte-initialized| & set of function (none) & Generate annotations
for initialization for the given set of functions \\
\hline
\lstinline |-rte-mem| & boolean (true) & Generate annotations for validity of
left-values access \\
\hline
\lstinline |-rte-pointer-call| & boolean (true) & Generate annotations for
validity of calls via function pointers \\
\hline
\lstinline|-rte-shift| & boolean (true) & Generate annotations for left and
right shift value out of bounds \\
\hline
\lstinline |-rte-select| & set of function (all) & Run plug-in on a subset of C
functions \\
\hline
\lstinline |-rte-trivial-annotations| & boolean (false) & Generate all
annotations even when they trivially hold \\
\hline
\lstinline |-rte-warn| & boolean (true) & Emit warning on broken annotations \\
\hline
\end{tabular}
\caption{\rte{} options} \label{options}
\end{center}
\end{table}
\cleardoublepage \cleardoublepage
\phantomsection \phantomsection
......
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