From 0de3f51385212ca0d1ff88fe5051e86f477084c4 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 9 Apr 2021 14:57:14 +0200
Subject: [PATCH] [Doc] fixes and improvements to userman
---
doc/userman/user-compliance.tex | 50 ++++++++++++++++++---------------
1 file changed, 27 insertions(+), 23 deletions(-)
diff --git a/doc/userman/user-compliance.tex b/doc/userman/user-compliance.tex
index d9aaecfc8b4..c8960acda58 100644
--- a/doc/userman/user-compliance.tex
+++ b/doc/userman/user-compliance.tex
@@ -55,17 +55,17 @@ cases, we simply refer to the related section in the ISO C standard.
\endfoot
\label{tab:undefined-unspecified-behaviors}%
\texttt{-warn-invalid-bool} & Toggles reporting of UB {\em CC.12} when applied to values of type \texttt{\_Bool}. \\
- \texttt{-warn-invalid-pointer} & Toggles reporting of UB {\em CC.46}. \\
+ \texttt{-warn-invalid-pointer} & Toggles reporting of UBs {\em CC.46} and {\em CC.62}. \\
\texttt{-warn-left-shift-negative} & Toggles reporting of UB {\em CC.52}. \\
\texttt{-warn-pointer-downcast} & Toggles reporting of UB {\em CC.24}. \\
- \texttt{-warn-right-shift-negative} & Toggles reporting of the IDB mentioned in C11 \S 6.2.3.2. \\
- \texttt{-warn-signed-downcast} & Toggles reporting of UB {\em CC.17} for signed types, when converting from a wider to a narrower type. \\
- \texttt{-warn-signed-overflow} & Toggles reporting of UB {\em CC.17} for operations on signed types (except when converting from a wider to a narrower type). \\
- \texttt{-warn-unsigned-downcast} & Toggles reporting of UB {\em CC.17} for unsigned types, when converting from a wider to a narrower type. \\
- \texttt{-warn-unsigned-overflow} & Toggles reporting of a situation similar to UB {\em CC.17}, for operations on {\em unsigned} types, even though they are allowed by C11. \\
- \texttt{-initialized-padding-locals} & Toggles UnsB related to {\em DD.10} and {\em DD.13} for local variables. \\
- \texttt{-eva-initialization-padding-globals} & Controls UnsB related to {\em DD.10} and {\em DD.13} for the initialization status of padding in global variables. \\
- \texttt{-eva-warn-signed-converted-downcast} & Toggles warnings related to UB {\em CC.48}. \\
+ \texttt{-warn-right-shift-negative} & Toggles reporting of the IDB mentioned in C11 \S 6.5.7.5. \\
+ \texttt{-warn-signed-downcast} & Toggles reporting of UB {\em CC.36} for signed types, when converting from a wider to a narrower type. \\
+ \texttt{-warn-signed-overflow} & Toggles reporting of UB {\em CC.36} for operations on signed types (except when converting from a wider to a narrower type). \\
+ \texttt{-warn-unsigned-downcast} & Toggles reporting of UB {\em CC.36} for unsigned types, when converting from a wider to a narrower type. \\
+ \texttt{-warn-unsigned-overflow} & Toggles reporting of a situation similar to UB {\em CC.36}, for operations on {\em unsigned} types, even though they are allowed by C11. \\
+ \texttt{-initialized-padding-locals} & Toggles UnsB related to {\em DD.10} for local variables. \\
+ \texttt{-eva-initialization-padding-globals} & Controls UnsB related to {\em DD.10} for the initialization status of padding in global variables. \\
+ \texttt{-eva-warn-pointer-subtraction} & Toggles warnings related to UB {\em CC.48}. \\
\texttt{-eva-warn-undefined-pointer-comparison} & Toggles warnings related to pointer comparisons (related to UB {\em CC.53}). \\
\end{longtable}
@@ -88,18 +88,23 @@ emitted by the Eva plugin and C undefined behaviors.
\label{tab:rte}%
bool\_value & {\em CC.12} & All values other than $\{0, 1\}$ are trap representations for the \texttt{\_Bool} type. \\
dangling\_pointer & {\em CC.9}, {\em CC.10}, {\em CC.177} & \\
- differing\_blocks & {\em CC.48}, {\em CC.53} & \\
+ differing\_blocks & {\em CC.48} & \\
division\_by\_zero & {\em CC.45} & \\
float\_to\_int & {\em CC.17} & \\
function\_pointer & {\em CC.26}, {\em CC.41} & \\
freeable & {\em CC.179} & This is not an RTE category, but an alarm related to an ACSL precondition \\
- index\_bound & {\em CC.49}, {\em CC.176} (among others) & \\
- initialization & {\em CC.11}, {\em CC.180} & \\
- initialization\_of\_union & {\em CC.11}, {\em CC.180} & \\
- mem\_access & {\em CC.33}, {\em CC.62}, {\em CC.64} & \\
- overflow & {\em CC.36}, {\em CC.50} & For {\em CC.50}, see {\em Note about \texttt{ptrdiff\_t}}. \\
+ index\_bound & {\em CC.49} & \\
+ initialization & {\em CC.11}, {\em CC.21}, {\em CC.180} & \\
+ mem\_access & {\em CC.33}, {\em CC.43}, {\em CC.47}, {\em CC.62}, {\em CC.64}, {\em CC.176} (among others) & \\
+ overflow & {\em CC.24}, {\em CC.36}, {\em CC.50} &
+ This category comprises the following RTEs:
+ \texttt{signed\_overflow}, \texttt{unsigned\_overflow},
+ \texttt{signed\_downcast} and \texttt{unsigned\_downcast}
+ (mostly related to {\em CC.36}), and
+ \texttt{pointer\_downcast} (related to {\em CC.24}).
+ For {\em CC.50}, see {\em Note about \texttt{ptrdiff\_t}}. \\
overlap & {\em CC.54} & {\em CC.100} is handled by \FramaC's libc ACSL specifications. \\
- pointer\_value & {\em CC.46}, {\em CC.47}, {\em CC.62} & \\
+ pointer\_value & {\em CC.46}, {\em CC.62} & \\
ptr\_comparison & {\em CC.53} & \\
separation & {\em CC.35} & \\
shift & {\em CC.51}, {\em CC.52} & \\
@@ -140,10 +145,9 @@ For a few UBs of syntactic nature, which are always detected during compilation,
will generate an error during compilation anyway, {\em without} requiring
specific compilation flags.
-This list is not exhaustive; some UBs not listed here are partially handled
-by \FramaC. Others require further analysis to determine whether some \FramaC
-analyzer handles them. Please contact the \FramaC team if you would like more
-information about whether a specific set of UBs is handled by the platform.
+This list is not exhaustive; in particular, some UBs not listed here are
+partially handled by \FramaC. Please contact the \FramaC team if you would like
+more information about whether a specific set of UBs is handled by the platform.
\begin{longtable}{>{\raggedright}m{0.1\textwidth} m{0.9\textwidth} >{\raggedright\arraybackslash}m{0.3\textwidth}}
\caption{%
@@ -177,7 +181,7 @@ information about whether a specific set of UBs is handled by the platform.
\section{Common Weakness Enumerations (CWEs) Reported and not Reported by Frama-C}
-This section lists some CWEs which \FramaC is known to handle, as well as some
+This section lists some CWEs handled by \FramaC, as well as some
which are currently out of the scope of \FramaC's default plugins. The latter
may be handled by specialized analyses, such as plugins not currently
distributed with the open-source release of \FramaC, or in future evolutions
@@ -200,7 +204,7 @@ in Juliet's 1.3 C/C++ test suite, available at NIST SAMATE's website.
Several caveats apply; for instance, some Juliet tests marked as {\em bad}
(that is, exhibiting a weakness) only do so for specific architectural
configurations, e.g. 32-bit pointers. If \FramaC is run with a different
-\texttt{machdep}, the test may not exhibit any undefined behavior, thus
+\texttt{machdep}, the test may not exhibit any undefined behavior, as
the weakeness is not actually present for such architectures.
A rigorous assessment of such situations is necessary for strong claims of
soundness.
@@ -296,7 +300,7 @@ handling of the CWE by \FramaC, as one of the following:
CWE-426: Untrusted Search Path & Not Handled & Not UB-related; requires annotations\\
CWE-427: Uncontrolled Search Path Element & Annotations & Requires annotating path-related functions and untrusted sources\\
CWE-440: Expected Behavior Violation & Too Vague & -\\
- CWE-457: Use of Uninitialized Variable & Handled & See remarks about {\em DD.10} and {\em DD.13}\\
+ CWE-457: Use of Uninitialized Variable & Handled & See remarks about {\em DD.10}\\
CWE-459: Incomplete Cleanup & Annotations & Requires annotating resources and cleanup functions\\
CWE-464: Addition of Data Structure Sentinel & Not Handled & -\\
CWE-467: Use of sizeof on a Pointer Type & Syntactic & -\\
--
GitLab