diff --git a/doc/rte/rte.tex b/doc/rte/rte.tex index 260b1e10663f2fa95a2e86e59ce0a5e7d5c10834..8db61fe2d610d776a453f8364727b9eb9bb92af7 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 @@ -817,6 +820,9 @@ right shift on negative values \\ \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}