[Kernel] Documents new options -warn-invalid-pointer and -warn-pointer-downcast.

In the user manual and in the man page.

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 dereference of an invalid pointer
+  \emph{always} generate an alarm.
+
+  For instance, no error is detected by default in the following example, as
+  the dereference 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

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)}

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.