diff --git a/doc/userman/user-analysis.tex b/doc/userman/user-analysis.tex index d82d08717a8db34d15bfc3a9859f8b71cf5e3243..89fdc0a9b599051aec566618ee018f0022e0ece5 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 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 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/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.