From 70f692b56f0ba3612824f214242caf41b28ba3a1 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 13 Apr 2021 16:25:41 +0200
Subject: [PATCH] [rte/doc] Fixes documentation
---
doc/rte/rte.tex | 38 ++++++++++++++++++++++----------------
src/plugins/rte/options.ml | 2 +-
src/plugins/rte/rte.ml | 2 +-
3 files changed, 24 insertions(+), 18 deletions(-)
diff --git a/doc/rte/rte.tex b/doc/rte/rte.tex
index 03d9dc53276..1a38e911173 100644
--- a/doc/rte/rte.tex
+++ b/doc/rte/rte.tex
@@ -7,6 +7,9 @@
\newcommand{\optnodowncast}{\mbox{\lstinline|-rte-no-downcast|}}
\newcommand{\rte}{\textsf{RTE}\xspace}
\newcommand{\framac}{\textsf{Frama-C}\xspace}
+\newcommand{\acsl}{\textsf{ACSL}\xspace}
+\newcommand{\gcc}{\textsf{Gcc}\xspace}
+\newcommand{\clang}{\textsf{Clang}\xspace}
\tableofcontents
@@ -443,7 +446,7 @@ Dereferencing a pointer is an undefined behavior if:
\end{itemize}
The \rte{} plug-in generates annotations to prevent this type of undefined
-behavior in a systematic way. It does so by deferring the check to the ACSL
+behavior in a systematic way. It does so by deferring the check to the \acsl{}
built-in predicate \lstinline|valid(p)|: \lstinline|valid(s)| (where
\lstinline|s| is a set of terms) holds if and only if dereferencing any
$\lstinline|p| \in \lstinline|s|$ is safe (i.e. points to a safely allocated
@@ -681,7 +684,7 @@ int f(float v) {
\section{Expressions not considered by \rte{}}
An expression which is the operand of a \lstinline|sizeof| (or
-\lstinline|__alignof|, a GCC operator parsed by Cil) is ignored by \rte{}, as
+\lstinline|__alignof|, a \gcc{} operator parsed by Cil) is ignored by \rte{}, as
are all its sub-expressions. This is an approximation, since the operand of
\lstinline|sizeof| may sometimes be evaluated at runtime, for instance on
variable sized arrays: see the example in \cnn{} paragraph \mbox{6.5.3.4.7}.
@@ -740,8 +743,8 @@ int main(void)
\section{Initialization}
-Reading an uninitialized value can be an undefined behavior. Mostly two general
-cases apply:
+Reading an uninitialized value can be an undefined behavior in the two following
+cases:
\begin{itemize}
\item \mbox{ISO C11 6.3.2.1}\footnote{here we use C11 as it is clearer than C99}
@@ -750,10 +753,10 @@ cases apply:
that it was a trap representation for the type used for the access.
\end{itemize}
-The second item is the consequence of the fact that an uninitialized location
-has indeterminate value (\mbox{6.7.9.10}), thus either an unspecified value or
-a trap representation, and that reading a trap representation is an undefined
-behavior (\mbox{6.2.6.1.5}).
+More generally, reading an uninitialized location always results in an
+indeterminate value (\mbox{6.7.9.10}). Such a value is either an unspecified
+value or a trap representation. Only reading a trap representation is an
+undefined behavior (\mbox{6.2.6.1.5}). It corresponds to the second case above.
However for (most) types that do not have trap representation, reading an
unspecified value is generally not a desirable behavior. Thus, \rte{} is
@@ -765,19 +768,20 @@ a typedef of those) is read, it must be initialized except if it is a formal
parameter or a global variable. We exclude formal parameters as its
initialization status must be checked at the call point (\rte{} generates an
annotation for this). We exclude global variables as they are initialized by
-default and any value stored in this variable must be initialized (and \rte{}
+default and any value stored in this variable must be initialized (\rte{}
generates an annotation for this).
As structures and unions never have trap representation, they can (and they are
regularly) be manipulated while being partially initialized. Consequently,
-\rte{} does not requires initialization for reads of a full union or structure
-(while read field with fundamental types are covered by the previous paragraph).
-As a consequence, the case of a structure or union \textit{whose address is never
- taken is read before being initialized} is \textbf{not} covered by \rte{}. But
+\rte{} does not require initialization for reads of a full union or structure
+(while reading fields with fundamental types is covered by the previous paragraph).
+As a consequence, the case of structures and unions \textit{whose address is
+ never taken, and being read before being initialized} is \textbf{not} covered
+by \rte{}. It is worth noting that
this particular case is efficiently detected by a compiler warning (see
-\lstinline{-Wuninitialized} on GCC and Clang for example) as it only requires
-local reasoning that is easy for compilers (but not that simple to express in
-ACSL).
+\lstinline{-Wuninitialized} on \gcc{} and \clang{} for example) as it only
+requires local reasoning that is easy for compilers (but not that simple to
+express in \acsl{}).
If you really need \rte{} to cover the previous case, please contact the
Frama-C team.
@@ -787,6 +791,8 @@ cannot have trap representation (for example \lstinline{unsigned char}) should
be allowed, for example writing a \lstinline{memcpy} function. In this case, one
can exclude this function from the range of function annotated with
initialization properties using \lstinline{-rte-initialized-ignore}.
+Note that the excluded functions must preserve the initialization of globals, as
+no assertions are generated for them.
\section{Undefined behaviors not covered by \rte{}}
diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml
index 0adbf3b1961..98d4a4285b2 100644
--- a/src/plugins/rte/options.ml
+++ b/src/plugins/rte/options.ml
@@ -68,7 +68,7 @@ module DoInitialized =
(struct
let option_name = "-rte-initialized"
let help = "when on, annotates local variables and pointers \
- reads of non struct types with initialization tests \
+ reads of non struct or union types with initialization tests \
see documentation for more details."
end)
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index a749c37f680..b1d99f4d059 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -110,7 +110,7 @@ let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
match lv with
| Var vi, NoOffset ->
(** Note: here [lv] has structure/union type or fundamental type.
- We exclude structure and unions. And for fundamental types:
+ We exclude structures and unions. And for fundamental types:
- globals (initialized and then only written with initialized values)
- formals (checked at function call)
- temporary variables (initialized during AST normalization)
--
GitLab