Skip to content
Snippets Groups Projects
Commit ad79216a authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[Doc] update table of RTE/UB correspondence

parent f727f157
No related branches found
No related tags found
No related merge requests found
......@@ -131,7 +131,7 @@ cases, we simply refer to the related section in the ISO C standard.
This section presents the correspondence between runtime execution (RTE) alarms
emitted by the Eva plugin and C undefined behaviors.
\begin{longtable}{>{\raggedright}m{0.26\textwidth} >{\raggedright\arraybackslash}m{0.28\textwidth} >{\raggedright\arraybackslash}m{0.4\textwidth}}
\begin{longtable}{>{\raggedright}m{0.20\textwidth} >{\raggedright\arraybackslash}m{0.26\textwidth} >{\raggedright\arraybackslash}m{0.46\textwidth}}
\caption{%
Correspondence between \FramaC's runtime error categories and C's undefined behaviors.
}\\
......@@ -146,7 +146,7 @@ emitted by the Eva plugin and C undefined behaviors.
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 \\
freeable & {\em CC.179} & This is not an RTE category, but an alarm related to an ACSL precondition. \\
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) & Alignment issues are currently not reported by Frama-C. \\
......@@ -160,7 +160,7 @@ emitted by the Eva plugin and C undefined behaviors.
overlap & {\em CC.54} & {\em CC.100} is handled by \FramaC's libc ACSL specifications. \\
pointer\_value & {\em CC.46}, {\em CC.62} & \\
ptr\_comparison & {\em CC.53} & \\
separation & {\em CC.35} & \\
separation & & Related to ACSL memory separation hypotheses. \\
shift & {\em CC.51}, {\em CC.52} & \\
special\_float & & Non-finite floating-point values are not UB, but can be optionally considered as undesirable. \\
\end{longtable}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment