diff --git a/doc/rte/rte.tex b/doc/rte/rte.tex
index 260b1e10663f2fa95a2e86e59ce0a5e7d5c10834..228c049928b7299a356944ebcf38e546b939b0ae 100644
--- a/doc/rte/rte.tex
+++ b/doc/rte/rte.tex
@@ -805,6 +805,9 @@ signed overflows \\
\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
@@ -814,9 +817,12 @@ right shift on negative values \\
\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
+\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}
diff --git a/doc/userman/user-analysis.tex b/doc/userman/user-analysis.tex
index d82d08717a8db34d15bfc3a9859f8b71cf5e3243..926fc9eecd7aba7b21d073d120f60b8fa075ed65 100644
--- a/doc/userman/user-analysis.tex
+++ b/doc/userman/user-analysis.tex
@@ -152,6 +152,23 @@ With \texttt{-safe-arrays}, the two accesses to \lstinline|v| are considered
invalid. (Accessing \lstinline|v.b[-2]| or \lstinline|v.b[3]| remains incorrect,
regardless of the value of the option.)
+\item \optiondef{-}{warn-invalid-pointer} may be used to check that the code
+ does not perform illegal pointer arithmetics, creating pointers that do not
+ point inside an object or one past an object.
+ This option is disabled by default, allowing the creation of such invalid
+ pointers without alarm — but the dereferencing of an invalid pointer
+ \emph{always} generates an alarm.
+
+ For instance, no error is detected by default in the following example, as
+ the dereferencing is correct. However, if option
+ \texttt{-warn-invalid-pointer} is enabled, an error is detected at line 4.
+ \begin{ccode}
+ int x;
+ int *p = &x;
+ p++; // valid
+ p++; // undefined behavior
+ *(p-2) = 1;
+ \end{ccode}
\item \optiondef{-}{unspecified-access} may be used to check when the
evaluation of an expression depends on the order in which its sub-expressions
@@ -179,6 +196,16 @@ Here, the \texttt{x} might be incremented by \texttt{g} before or after the
call to \texttt{f}, but since the two write accesses occur in different
functions, \texttt{-unspecified-access} does not detect that.
+\item \optiondef{-}{warn-pointer-downcast} may be used to check that the code
+ does not downcast a pointer to an integer type. This option is set by default.
+ In the following example, analyzers report by default an error on the third
+ line. Disabling the option removes this verification.
+ \begin{ccode}
+ int x;
+ uintptr_t addr = &x;
+ int a = &x;
+ \end{ccode}
+
\item \optiondef{-}{warn-signed-downcast} may be used to check that the analyzed
code does not downcast an integer to a signed integer type. This option is
\emph{not} set by default. Without it, the analyzers do not perform such a
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 75f767128b9a43f7c8fcb74845682e116f525124..262793fefb00e8968e01dcd6d1ca49469bea9ede 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -8,6 +8,8 @@ release. First we list changes of the last release.
\begin{itemize}
\item \textbf{Preparing the Sources:} added option
\texttt{-cpp-extra-args-per-file}.
+\item \textbf{Customizing Analyzers:} added options
+ \texttt{-warn-invalid-pointer} and \texttt{-warn-pointer-downcast}
\end{itemize}
\section*{20.0 (Calcium)}
diff --git a/doc/value/examples/alarms/pointer_arith.c b/doc/value/examples/alarms/pointer_arith.c
new file mode 100644
index 0000000000000000000000000000000000000000..2f66edd726d773f051d666f75e3d0994b882f3b4
--- /dev/null
+++ b/doc/value/examples/alarms/pointer_arith.c
@@ -0,0 +1,5 @@
+void main () {
+ int x, *p = &x;
+ p++;
+ p++;
+}
diff --git a/doc/value/examples/alarms/pointer_conversion.c b/doc/value/examples/alarms/pointer_conversion.c
new file mode 100644
index 0000000000000000000000000000000000000000..599a1f8645ca656e01b33bfa3237445c790647b0
--- /dev/null
+++ b/doc/value/examples/alarms/pointer_conversion.c
@@ -0,0 +1,7 @@
+#include <stdint.h>
+void main () {
+ char c;
+ uintptr_t a = &c;
+ char *p = (char *) (a + 1);
+ char *q = (char *) (a + 2);
+}
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 7db1b55844c7dc5fa286d68c1abde5f2e20a60ab..dd2d364f61eeca2ee6cb90b14e125fd39e523282 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -31,6 +31,7 @@
\newcommand{\framacversion}%
{\input{../../VERSION} (\input{../../VERSION_CODENAME}\unskip)}
+\newcommand{\isoc}{\textsf{C99}}
\newcommand{\Eva}{\textsf{Eva}}
@@ -630,7 +631,7 @@ no run-time error could happen when running the program.
The alarm means that \Eva{} could not prove that the value \verb|ks[i]|
accessed in \verb|skein_block.c:69| was definitely initialized before being
read. Reading an initialized value is an undefined behavior according to the
-ISO C99 standard (and can even lead to security vulnerabilities).
+\isoc{} standard (and can even lead to security vulnerabilities).
As is often the case, this alarm is related to the approximation introduced
in \verb|skein_block.c:56|, which is the loop responsible for initializing
@@ -1460,6 +1461,58 @@ to the attitude described in \ref{norme_pratique}. An option
to warn about these lines could happen if there was demand for
this feature.
+\subsubsection{Invalid pointer arithmetic}
+
+By default, \Eva{} does \emph{not} emit alarms on invalid pointer arithmetic:
+alarms are only emitted when an invalid pointer is dereferenced or wrongly used
+in a comparison, not at the creation of such pointers.
+
+However, if the \lstinline|-warn-invalid-pointer| option is enabled,
+\Eva{} emits an alarm when an operation may create a pointer that does
+not point inside an object or one past an object,
+even if this pointer is not used afterward.
+
+This may happen on:
+\begin{itemize}
+\item addition (or subtraction) of an integer from a pointer, when the analysis
+ is unable to prove that the resulting pointer points inside, or one past,
+ the same object pointed to by the initial pointer.
+ In this case, the emitted alarm reports a possible undefined behavior.
+\item conversion of an integer into a pointer. Except for the constant~0,
+ such a conversion is always an implementation-defined behavior
+ according to the \isoc{} standard. However, a footnote also explains that
+ conversion between pointers and integers is ``\emph{intended to
+ be consistent with the addressing structure of the execution environment}''.
+ This is why Eva also also authorizes conversion of integers:
+ \begin{itemize}
+ \item in the range of valid absolute addresses
+ (according to \texttt{absolute-valid-range})
+ \item computed from the address of an object \lstinline|o| such that the
+ resulting pointer points inside or one past the object \lstinline|o|.
+ \end{itemize}
+ In all other cases, an alarm is emitted, which reports the possible
+ implementation-defined behavior mentioned above.
+\end{itemize}
+
+In the example below, the first increment of the pointer \lstinline|p| is valid,
+although the resulting pointer should not be dereferenced. The second increment
+leads to an invalid alarm when option \lstinline|-warn-invalid-pointer| is on.
+\listinginput{1}{examples/alarms/pointer_arith.c}
+\begin{logs}
+ [eva:alarm] pointer_arith.c:4: Warning:
+ invalid pointer creation. assert \object_pointer(p + 1);
+\end{logs}
+
+In the same way, in the example below, the first conversion at line~5
+does not generate an alarm, but the second conversion leads to an invalid alarm
+with option \lstinline|-warn-invalid-pointer|.
+
+\listinginput{1}{examples/alarms/pointer_conversion.c}
+\begin{logs}
+ [eva:alarm] pointer_arith.c:6: Warning:
+ invalid pointer creation. assert \object_pointer((char *)(a + 2));
+\end{logs}
+
\subsubsection{Division by zero}
When dividing by an expression that the analysis
@@ -1494,7 +1547,7 @@ simpler than this one. Do not be surprised by them.
Another arithmetic alarm is the alarm emitted for logical
shift operations on integers where the second operand may be
larger than the size in bits of the first operand's type.
-Such an operation is left undefined by the ISO/IEC 9899:1999 standard, and
+Such an operation is left undefined by the \isoc{} standard, and
indeed, processors are often built in a way that such an
operation does not produce the \lstinline|0| or \lstinline|-1|
result that could have been expected. Here is an example
@@ -1506,7 +1559,7 @@ shift.c:4: ... invalid RHS operand for shift. assert 0 <= c < 32;
\Eva{} also detects shifts on negative integers.
Left-shifting a negative integer is an undefined behavior according to the
-ISO C99 standard, and leads to an alarm by default.
+\isoc{} standard, and leads to an alarm by default.
These alarms can be disabled by using the option
\lstinline|-no-warn-left-shift-negative|.
Right-shifting a negative integer is an implementation-defined operation,
@@ -1525,7 +1578,7 @@ By default, \Eva{} emits alarms for --- and reduces the
sets of possible results of --- signed arithmetic computations where
the possibility of an overflow exists. Indeed,
such overflows have an undefined behavior according to
-paragraph 6.5.5 of the ISO/IEC 9899:1999 standard.
+paragraph 6.5.5 of the \isoc{} standard.
%
If useful, it is also possible to assume that signed integers overflow
according to a 2's complement representation. The option
@@ -1536,10 +1589,16 @@ as potentially overflowing. This warning can also be disabled by option
By default, no alarm is emitted for arithmetic operations on unsigned integers
for which an overflow may happen, since such operations have
-defined semantics according to the ISO/IEC 9899:1999 standard.
+defined semantics according to the \isoc{} standard.
If one wishes to signal and prevent such unsigned overflows,
option \verb+-warn-unsigned-overflow+ can be used.
+By default, Eva emits alarms for downcasts of pointer values to (signed
+or unsigned) integer types. Such downcasts are indeed undefined behavior
+according to section 6.3.2.3, §6 of the \isoc{} standard.
+However, option \lstinline|-no-warn-pointer-downcast| can be used to disable
+these alarms.
+
Finally, by default, no alarm is emitted for downcasts to signed or unsigned
integers. In the signed case, the least significant bits
of the original value are used, and are interpreted according
@@ -1658,7 +1717,7 @@ of the call.
By default, \Eva{} emits an alarm whenever a trap representation might be read
from an lvalue of type \texttt{\_Bool}.
-According to the ISO/IEC 9899:1999 standard, the \texttt{\_Bool} type contains
+According to the \isoc{} standard, the \texttt{\_Bool} type contains
the values 0 and 1, but any other value might be a trap representation, that is,
an object representation that does not represent a valid value of the type.
Trap representations can be created through unions or pointer casts.
@@ -1810,7 +1869,7 @@ compiler, if we may ask such a rhetorical
question, is right? They all are, because the program is undefined.
When function \lstinline|copy()| is called from \lstinline|main()|,
the assignment \lstinline|*p = *q;| breaks
-C99's 6.5.16.1:3 rule. This rule states that
+\isoc{}'s 6.5.16.1:3 rule. This rule states that
in an assignment from lvalue to lvalue,
the left and right lvalues must overlap either exactly or not at all.
@@ -2116,7 +2175,7 @@ limited form, but imprecisions may accumulate quickly
\Eva{} does not check all the properties that could be
expected of it\footnote{There are 245 unspecified or undefined
- behaviors in Annex J of the ISO C99 standard.}. Support for each of
+ behaviors in Annex J of the \isoc{} standard.}. Support for each of
these missing features could arrive if the need was expressed. Below
are some of the existing limitations.
diff --git a/man/frama-c.1 b/man/frama-c.1
index 706d54135e1785b604e998aaccc3522b72559ceb..0fa77b175c62a1cc67debb77d2c4654444e360fd 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -25,7 +25,7 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2020-03-05
+.TH FRAMA-C 1 2020-04-02
.SH NAME
.PP
frama\-c[.byte] \- a static analyzer for C programs
@@ -737,6 +737,12 @@ parser:decimal\-float=once\f[] (and variants) instead.
.RS
.RE
.TP
+.B [\-no]\-warn\-invalid\-pointer
+generate alarms for invalid pointer arithmetic.
+Defaults to no.
+.RS
+.RE
+.TP
.B [\-no]\-warn\-left\-shift\-negative
generate alarms for signed left shifts on negative values.
Defaults to yes.
@@ -749,6 +755,13 @@ Defaults to no.
.RS
.RE
.TP
+.B [\-no]\-warn\-pointer\-downcast
+generates alarms when the downcast of a pointer may exceed the
+destination range.
+Defaults to yes.
+.RS
+.RE
+.TP
.B [\-no]\-warn\-signed\-downcast
generates alarms when signed downcasts may exceed the destination range.
Defaults to no.
diff --git a/man/frama-c.1.header b/man/frama-c.1.header
index ce56197c3e948b460514eedb2979d4a8b162ebe7..235124894053d3e0cceaa86f8793860a090af0d0 100644
--- a/man/frama-c.1.header
+++ b/man/frama-c.1.header
@@ -25,4 +25,4 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2020-03-05
+.TH FRAMA-C 1 2020-04-02
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index c5835e67eb2679f7bd0c620019070b21d54f4761..319c04fc20a3670566a429c73c2393888942264f 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -450,12 +450,19 @@ the case (this is the default).
**Deprecated**: use **-kernel-warn-key parser:decimal-float=once**
(and variants) instead.
+[-no]-warn-invalid-pointer
+: generate alarms for invalid pointer arithmetic. Defaults to no.
+
[-no]-warn-left-shift-negative
: generate alarms for signed left shifts on negative values. Defaults to yes.
[-no]-warn-right-shift-negative
: generate alarms for signed right shifts on negative values. Defaults to no.
+[-no]-warn-pointer-downcast
+: generates alarms when the downcast of a pointer may exceed the destination
+range. Defaults to yes.
+
[-no]-warn-signed-downcast
: generates alarms when signed downcasts may exceed the destination range.
Defaults to no.