diff --git a/doc/MakeLaTeXModern b/doc/MakeLaTeXModern
index 71107267b78246501afda730da7418313338c647..3ce60c391f19c7c56ae4c73e94dd7c02865343f4 100644
--- a/doc/MakeLaTeXModern
+++ b/doc/MakeLaTeXModern
@@ -1,5 +1,5 @@
FRAMAC_DOC_ROOT_DIR?=..
-FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf frama-c-affiliation.tex
+FRAMAC_MODERN=frama-c-book.cls frama-c-cover.pdf frama-c-left.pdf frama-c-right.pdf frama-c-affiliation.tex eu-flag.jpg anr-logo.png
frama-c-book.cls: $(FRAMAC_DOC_ROOT_DIR)/frama-c-book.cls
@rm -f $@
@@ -30,3 +30,15 @@ frama-c-affiliation.tex: $(FRAMAC_DOC_ROOT_DIR)/frama-c-affiliation.tex
@cp $< .
@chmod a-w $@
@echo "import $<"
+
+eu-flag.jpg: $(FRAMAC_DOC_ROOT_DIR)/eu-flag.jpg
+ @rm -f $@
+ @cp $< .
+ @chmod a-w $@
+ @echo "import $<"
+
+anr-logo.png: $(FRAMAC_DOC_ROOT_DIR)/anr-logo.png
+ @rm -f $@
+ @cp $< .
+ @chmod a-w $@
+ @echo "import $<"
diff --git a/doc/anr-logo.png b/doc/anr-logo.png
new file mode 100644
index 0000000000000000000000000000000000000000..ccdb43a8e595eff510c6d06b6ebe14aa54721efe
Binary files /dev/null and b/doc/anr-logo.png differ
diff --git a/doc/developer/.gitignore b/doc/developer/.gitignore
index a8469496d265792a2f0949dad390b0c1dc398303..092d8112a268d78e22984f9c0bf676a00feb4ab5 100644
--- a/doc/developer/.gitignore
+++ b/doc/developer/.gitignore
@@ -1,4 +1,6 @@
+/anr-logo.png
/developer.pdf
+/eu-flag.jpg
/frama-c-book.cls
/frama-c-cover.pdf
/frama-c-left.pdf
@@ -8,12 +10,6 @@
/tutorial/viewcfg/generated/
/tutorial/hello/generated/
/examples/generated/
-developer.pdf
-frama-c-book.cls
-frama-c-cover.pdf
-frama-c-left.pdf
-frama-c-right.pdf
-hello_world/
*.idx
*.out
developer.fdb_latexmk
diff --git a/doc/eu-flag.jpg b/doc/eu-flag.jpg
new file mode 100644
index 0000000000000000000000000000000000000000..d59420b9cdcd1ff44ef33c9860fb93f068e5ebd5
Binary files /dev/null and b/doc/eu-flag.jpg differ
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index 159783c66b38ec3bd23193d4ff238bbefe8e0a46..2dce074dba3e88dfbdcbf4accf40649dc42ece9e 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -39,7 +39,7 @@ prefix=framacbook@,
\RequirePackage[T1]{fontenc}
\RequirePackage[utf8]{inputenc}
\RequirePackage{amssymb}
-\RequirePackage{xcolor}
+\RequirePackage[table]{xcolor}
\RequirePackage[pdftex]{graphicx}
\RequirePackage{ifthen}
\RequirePackage{xspace}
@@ -128,6 +128,40 @@ prefix=framacbook@,
\medskip
\ifusecc\doclicenseThis\else\fi
}
+
+% \acknowledge{<flag image file>}{<text inside box>}
+\newcommand{\acknowledge}[2]{
+ \fbox{
+ \begin{minipage}{0.97\textwidth}
+ \begin{minipage}{1.2cm}
+ \includegraphics[width=\linewidth]{#1}
+ \end{minipage}
+ \begin{minipage}{0.90\textwidth}
+ This project has received funding from #2.
+ \end{minipage}
+ \end{minipage}
+ }
+}
+
+\newcommand{\acknowledgeANR}{
+ \acknowledge{anr-logo.png}{the French ANR projects
+ CAT~(ANR-05-RNTL-00301) and U3CAT~(08-SEGI-021-01)
+ }
+}
+
+\newcommand{\acknowledgeEU}{
+ \acknowledge{eu-flag.jpg}{the
+ European Union's Seventh Framework Programme (FP7/2007-2013)
+ under grant agreement N$^\circ$\,317753 (\mbox{STANCE}).\\
+ It has also received funding from the Horizon 2020 research
+ and innovation programme, under grant agreements
+ N$^\circ$\,731453~(\mbox{VESSEDIA}),
+ N$^\circ$\,824231~(\mbox{DECODER}),
+ N$^\circ$\,830892~(\mbox{SPARTA}),
+ and N$^\circ$\,883242~(\mbox{ENSURESEC})
+ }
+}
+
% --------------------------------------------------------------------------
% --- Sectionning ---
% --------------------------------------------------------------------------
diff --git a/doc/metrics/.gitignore b/doc/metrics/.gitignore
index 06c1c792c58efdabbee5c308a8da223fa4e5e78d..58acfccd3f95d479e49545c1041c63d0f4fbcef6 100644
--- a/doc/metrics/.gitignore
+++ b/doc/metrics/.gitignore
@@ -1,3 +1,5 @@
+/anr-logo.png
+/eu-flag.jpg
/frama-c-book.cls
/frama-c-cover.pdf
/frama-c-left.pdf
diff --git a/doc/pdg/.gitignore b/doc/pdg/.gitignore
index e9b8c33454088763484eba5e7f1613510710dbf6..62322591627fb455e5a5b654bb774d0a77856b8f 100644
--- a/doc/pdg/.gitignore
+++ b/doc/pdg/.gitignore
@@ -1,4 +1,6 @@
+anr-logo.png
biblio.bib
+eu-flag.jpg
frama-c-book.cls
frama-c-cover.pdf
frama-c-left.pdf
diff --git a/doc/release/.gitignore b/doc/release/.gitignore
index f5569bd78614424dfbe8379088183f6e1a5f4956..8590f2c47f97ebace19b519fd9329e39501fc4bc 100644
--- a/doc/release/.gitignore
+++ b/doc/release/.gitignore
@@ -1,3 +1,5 @@
+/anr-logo.png
+/eu-flag.jpg
/frama-c-book.cls
/frama-c-cover.pdf
/frama-c-left.pdf
diff --git a/doc/rte/.gitignore b/doc/rte/.gitignore
index 92f50e6b35d68a2b554aa3e2ff3783d0daf47760..77ccbb7eaf92e390d1162ea9f3af03b698423f9a 100644
--- a/doc/rte/.gitignore
+++ b/doc/rte/.gitignore
@@ -1,3 +1,5 @@
+/anr-logo.png
+/eu-flag.jpg
/frama-c-book.cls
/frama-c-cover.pdf
/frama-c-left.pdf
diff --git a/doc/slicing/.gitignore b/doc/slicing/.gitignore
index 1913f75af091fc85fd9142f3bab9583ee9561490..ed79c64d8ff52e771af67d7d1de8186cc5956922 100644
--- a/doc/slicing/.gitignore
+++ b/doc/slicing/.gitignore
@@ -1,4 +1,6 @@
+anr-logo.png
biblio.bib
+eu-flag.jpg
frama-c-book.cls
frama-c-cover.pdf
frama-c-left.pdf
diff --git a/doc/userman/.gitignore b/doc/userman/.gitignore
index f7fe0b371139f1dac67e7449fabe7c0b52a17614..a2dae99658f6339db386901d057bf1f5368eccf6 100644
--- a/doc/userman/.gitignore
+++ b/doc/userman/.gitignore
@@ -1,3 +1,5 @@
+anr-logo.png
+eu-flag.jpg
frama-c-book.cls
frama-c-cover.pdf
frama-c-left.pdf
diff --git a/doc/userman/macros.tex b/doc/userman/macros.tex
index 508f439cb76b5dd2fc05ff7744c7f083843c0157..89afeea7155d1c80625056be00277497f3a0a9fb 100644
--- a/doc/userman/macros.tex
+++ b/doc/userman/macros.tex
@@ -1,5 +1,5 @@
\newcommand{\framacversion}%
- {\input{../../VERSION} (\input{../../VERSION_CODENAME}\unskip)}
+ {\input{../../VERSION}\unskip{} (\input{../../VERSION_CODENAME}\unskip)}
\newcommand{\nextframacversion}{Frama-C+dev}
\newcommand{\tool}[1]{\textsf{#1}\xspace}
diff --git a/doc/userman/user-compliance.tex b/doc/userman/user-compliance.tex
new file mode 100644
index 0000000000000000000000000000000000000000..c9f47c9e90aa93eedbac37955f668e685115ff47
--- /dev/null
+++ b/doc/userman/user-compliance.tex
@@ -0,0 +1,396 @@
+%% --------------------------------------------------------------------------
+%% --- Analysis scripts
+%% --------------------------------------------------------------------------
+
+\chapter{Compliance}
+\label{user-compliance}
+
+\newcommand{\CWE}[1]{\href{https://cwe.mitre.org/data/definitions/#1.html}{CWE-#1}}
+
+% Macros used by the tables in this chapter
+\definecolor{lightgray}{gray}{0.9}
+% alternate rowcolors for all long-tables
+\let\oldlongtable\longtable
+\let\endoldlongtable\endlongtable
+\renewenvironment{longtable}{\rowcolors{2}{white}{lightgray}\oldlongtable} {
+\endoldlongtable}
+
+\FramaC provides sound analyses for several kinds of code defects.
+Given the large amount of covered defects and command-line options which
+toggle their reporting, we provide in this chapter information about standards
+compliance, coding guidelines and related documents, such as the ISO C standard,
+CWEs, CERT C, etc.
+
+This chapter is not exhaustive; in particular, some defects are implicitly
+checked without any controlling options; others may be affected by
+a combination of several options which is hard to precisely express.
+
+Please contact the \FramaC team if you require a thorough evaluation of the
+standards cited here, or of different ones. This reference is provided on a
+best-effort basis.
+
+\section{Frama-C Options Related to C Undefined Behaviors}
+
+This section lists several \FramaC options affecting (either enabling or
+disabling) the detection of {\em unspecified} and {\em undefined} behaviors
+listed in Annexes J.1 and J.2 of the C11 standard (ISO/IEC 9899:2011).
+
+Note: the ISO C standard does not provide an identifier for each behavior;
+therefore, we use the numbers listed in
+{\em SEI CERT C Coding Standard's Back Matter}, sections
+{\em CC. Undefined Behavior} and {\em DD. Unspecified Behavior}, whenever
+possible. These tables can be found at
+\url{https://wiki.sei.cmu.edu/confluence/display/c}.
+Note that SEI CERT does not list implementation-defined behaviors; in such
+cases, we simply refer to the related section in the ISO C standard.
+
+% ugly hack to force hyphenation inside \texttt, for the very long options
+\texttt{\hyphenchar\font=`\- \hyphenpenalty=10000 \exhyphenpenalty=-50}
+
+\begin{longtable}{m{0.42\textwidth} m{0.53\textwidth}}
+ \caption{Impact of some \FramaC options on a few unspecified and undefined
+ behaviors.}\\
+ \cellcolor{white}\textbf{{\em Command-line Option}} & \cellcolor{white}\textbf{{\em Affected behaviors}} \\
+ \hline
+ \endhead
+ \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 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.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}
+
+% disable the hyphenation ugly hack
+\texttt{\hyphenchar\font=-1}
+
+\section{RTE categories and C Undefined Behaviors}
+
+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}}
+ \caption{%
+ Correspondence between \FramaC's runtime error categories and C's undefined behaviors.
+ }\\
+ \cellcolor{white}\textbf{{\em RTE Category}} & \cellcolor{white}\textbf{{\em Related UBs}} & \cellcolor{white}\textbf{{\em Notes}} \\
+ \hline
+ \endhead
+ \endfoot
+ \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} & \\
+ 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} & \\
+ 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. \\
+ 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.62} & \\
+ ptr\_comparison & {\em CC.53} & \\
+ separation & {\em CC.35} & \\
+ 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}
+
+Note that some undefined behaviors,
+such as {\em CC.100}, {\em CC.191}, {\em CC.192} and others,
+are not handled by specific categories of RTEs, but instead by ACSL
+specifications in \FramaC's libc. These specifications are used by some
+analyzers and result in warnings and errors when violated.
+
+\paragraph{Note about \texttt{ptrdiff\_t}}
+ {\em CC.50} deals with pointer subtractions, related to type \texttt{ptrdiff\_t}.
+ \FramaC does not perform specific handling for this type,
+ but in all standard machdeps defined in \FramaC, its definition
+ is such that pointer subtraction will lead to a signed overflow
+ if the difference cannot be represented in \texttt{ptrdiff\_t},
+ thus preventing the undefined behavior. However, if option
+ \texttt{-no-warn-signed-overflow} is used, or in a custom machdep,
+ this may not hold.
+
+\section{C Undefined Behaviors {\em not} handled by \FramaC}
+
+This section lists some of the C undefined behaviors which are currently
+{\em not} directly covered by the open-source version of \FramaC.
+
+The list includes UBs which are delegated to other tools, such as the
+preprocessor or the compiler.
+\FramaC does not preprocess the sources, relying on external
+preprocessors such as GCC's or Clang; therefore, related UBs are out of the
+scope of \FramaC and listed below, even though in practice they are verified
+by the underlying preprocessor in all but the most exotic architectures.
+
+For a few UBs of syntactic nature, which are always detected during compilation,
+\FramaC delegates the task to the compiler. This implies that, when running
+\FramaC directly on the code, it may not complain about them; but the code
+will generate an error during compilation anyway, {\em without} requiring
+specific compilation flags.
+
+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{%
+ C undefined behaviors {\em not} handled by \FramaC.
+ }\\
+ \cellcolor{white}\textbf{{\em UB}} & \cellcolor{white}\textbf{{\em Notes}} \\
+ \hline
+ \endhead
+ \endfoot
+ \label{tab:ubs-not-handled}%
+ CC.2 & Syntactic; out of the scope of \FramaC's analyzers.\\
+ CC.3 & Out of scope (lexing/preprocessing-related).\\
+ CC.5 & Requires concurrency analysis; the Mthread plugin can provide some guarantees.\\
+ CC.14 & Only applies to implementations not following IEEE-754. \FramaC's machdeps assume they do.\\
+ CC.18 & Only applies to implementations not following IEEE-754. \FramaC's machdeps assume they do.\\
+ CC.27 & Out of scope (lexing/preprocessing-related).\\
+ CC.28 & Out of scope (lexing/preprocessing-related).\\
+ CC.30 & Out of scope (lexing/preprocessing-related).\\
+ CC.31 & Out of scope (lexing/preprocessing-related).\\
+ CC.34 & Out of scope (lexing/preprocessing-related).\\
+ CC.58 & Syntactic; delegated to the compiler.\\
+ CC.59 & Syntactic; delegated to the compiler.\\
+ CC.90 & Out of scope (lexing/preprocessing-related).\\
+ CC.91 & Out of scope (lexing/preprocessing-related).\\
+ CC.92 & Out of scope (lexing/preprocessing-related).\\
+ CC.93 & Out of scope (lexing/preprocessing-related).\\
+ CC.94 & Out of scope (lexing/preprocessing-related).\\
+ CC.95 & Out of scope (lexing/preprocessing-related).\\
+ CC.96 & Out of scope (lexing/preprocessing-related).\\
+\end{longtable}
+
+\section{Common Weakness Enumerations (CWEs) Reported and not Reported by Frama-C}
+
+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
+of the \FramaC platform.
+
+Note that, due to the large amount of existing CWEs, and the fact that mapping
+them to undefined behaviors is not always straightforward, there are likely
+several other CWEs which are already handled by \FramaC, at least in some
+contexts.
+Please contact the \FramaC team if you would like more information about whether
+a specific set of CWEs is handled by some analysis in the platform.
+
+Remark: this section is partially based on work related to
+NIST's Software Assurance Metrics and Tool Evaluation
+(SAMATE\footnote{\url{https://samate.nist.gov/Main_Page.html}}),
+namely its Static Analysis Tool Expositions (SATE),
+which allowed us to identify some of the CWEs which
+\FramaC already can or cannot handle. The CWEs listed here are mostly those
+present 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, as
+the weakeness is not actually present for such architectures.
+A rigorous assessment of such situations is necessary for strong claims of
+soundness.
+
+In Table~\ref{tab:cwe}, the {\em Status} column summarizes the current
+handling of the CWE by \FramaC, as one of the following:
+
+\begin{description}
+\item[Handled] means \FramaC already handles the CWE; in some cases, its
+ detection may be controlled by command-line options;
+\item[Partially Handled] means the CWE is handled only in some specific cases;
+ \FramaC can thus help {\em detect} occurrences of this CWE, but not
+ {\em prove their absence};
+\item[Annotations] means the CWE could be handled by \FramaC, but some
+ development is required; in practice, this often means user annotations
+ will be required, e.g. for specifying the source of tainted data;
+ this often implies adding a new abstract domain to Eva, or modifying the
+ analyzer to propagate the data provided by the annotations;
+\item[Syntactic] means the CWE is of a syntactic nature, while \FramaC
+ specializes in semantic analyses; it is currently not handled by \FramaC
+ and could probably be so, if a user required it; but it is not the primary
+ concern of the platform developers.
+\item[Too Vague] means the CWE is either too vague or too broad to be formally
+ matched to a given set of properties that \FramaC can verify.
+\end{description}
+
+{\small
+\begin{longtable}{>{\raggedright}m{0.42\textwidth} m{0.13\textwidth} >{\raggedright\arraybackslash}m{0.45\textwidth}}
+ \caption{%
+ CWEs handled and not currently handled by \FramaC's open-source plugins.
+ The {\em Notes} column may contain references to the command-line options
+ table (\ref{tab:undefined-unspecified-behaviors}).
+ The descriptions in the {\em Status} column are detailed above.
+ }\\
+ \cellcolor{white}\textbf{{\em CWE}} & \cellcolor{white}\textbf{{\em Status}} & \cellcolor{white}\textbf{{\em Notes}} \\
+ \hline
+ \endhead
+ \endfoot
+ \label{tab:cwe}%
+ \CWE{15}: External Control of System or Configuration Setting & Annotations & Requires annotating configuration settings and untrusted sources\\
+ \CWE{23}: Relative Path Traversal & Annotations & Requires annotating path-related functions and untrusted sources\\
+ \CWE{36}: Absolute Path Traversal & Annotations & Requires annotating path-related functions and untrusted sources\\
+ \CWE{78}: Improper Neutralization of Special Elements used in an OS Command ('OS Command Injection') & Annotations & Requires annotating which functions may inject OS commands\\
+ \CWE{90}: Improper Neutralization of Special Elements used in an LDAP Query ('LDAP Injection') & Annotations & Requires annotating which functions are LDAP-related\\
+ \CWE{114}: Process Control & Annotations & Requires annotating sensitive functions and untrusted sources\\
+ \CWE{119}: Improper Restriction of Operations within the Bounds of a Memory Buffer & Handled & -\\
+ \CWE{120}: Buffer Copy without Checking Size of Input ('Classic Buffer Overflow') & Handled & -\\
+ \CWE{121}: Stack-based Buffer Overflow & Handled & -\\
+ \CWE{122}: Heap-based Buffer Overflow & Handled & -\\
+ \CWE{123}: Write-what-where Condition & Handled & -\\
+ \CWE{124}: Buffer Underwrite & Handled & -\\
+ \CWE{125}: Out-of-bounds Read & Handled & -\\
+ \CWE{126}: Buffer Overread & Handled & -\\
+ \CWE{127}: Buffer Underread & Handled & -\\
+ \CWE{128}: Wrap-around Error & Handled & Toggled by options \texttt{-warn-signed-overflow}, \texttt{-warn-unsigned-overflow}, \texttt{-warn-signed-downcast} and \texttt{-warn-unsigned-downcast}.\\
+ \CWE{129}: Improper Validation of Array Index & Handled & -\\
+ \CWE{131}: Incorrect Calculation of Buffer Size & Handled & Reported not directly at the allocation site, but during usage; the GUI allows navigating back to the source.\\
+ \CWE{134}: Use of Externally-Controlled Format String & Annotations & Requires annotating which format strings come from external sources\\
+ \CWE{176}: Improper Handling of Unicode Encoding & Annotations & Requires annotating Unicode-related functions and variables\\
+ \CWE{188}: Reliance on Data Memory Layout & Partially Handled & \FramaC memory model handles some kinds of invalid accesses\\
+ \CWE{190}: Integer Overflow or Wraparound & Handled & See remarks about {\em CC.17} in Table~\ref{tab:undefined-unspecified-behaviors}\\
+ \CWE{191}: Integer Underflow & Handled & See remarks about {\em CC.17} in Table~\ref{tab:undefined-unspecified-behaviors}\\
+ \CWE{194}: Unexpected Sign Extension & Handled & See note about {\em Numerical Conversions}\\
+ \CWE{195}: Signed to Unsigned Conversion Error & Handled & See note about {\em Numerical Conversions}\\
+ \CWE{196}: Unsigned to Signed Conversion Error & Handled & See note about {\em Numerical Conversions}\\
+ \CWE{197}: Numeric Truncation Error & Handled & See note about {\em Numerical Conversions}\\
+ \CWE{222}: Truncation of Security Relevant Information & Not Handled & -\\
+ \CWE{223}: Omission of Security Relevant Information & Not Handled & -\\
+ \CWE{226}: Sensitive Information in Resource Not Removed Before Reuse & Annotations & Requires annotating shared resources and external entities\\
+ \CWE{242}: Use of Inherently Dangerous Function & Annotations & Requires annotating which functions are ``inherently dangerous''\\
+ \CWE{244}: Improper Clearing of Heap Memory Before Release ('Heap Inspection') & Not Handled & Semantic property unavailable at the C memory model; syntactic heuristics can be devised\\
+ \CWE{252}: Unchecked Return Value & Syntactic & -\\
+ \CWE{253}: Incorrect Check of Function Return Value & Syntactic + Annotations & Similar to \CWE{252}, but also requires annotations definining what ``correct check'' means\\
+ \CWE{256}: Unprotected Storage of Credentials & Annotations & Requires annotating credential-related functions and variables\\
+ \CWE{259}: Use of Hard-coded Password & Annotations & Requires annotating password-related functions and variables\\
+ \CWE{272}: Least Privilege Violation & Annotations & Requires annotating sensitive functions\\
+ \CWE{273}: Improper Check for Dropped Privileges & Annotations & Requires annotating sensitive functions and forbidden control paths\\
+ \CWE{284}: Improper Access Control & Annotations & Requires annotating privileges, permissions, control paths, etc.\\
+ \CWE{319}: Cleartext Transmission of Sensitive Information & Annotations & Requires annotating sensitive data and transmission-related functions\\
+ \CWE{321}: Hard Coded Cryptographic Key & Annotations & Requires annotating which data correspond to cryptographic keys\\
+ \CWE{325}: Missing Cryptographic Step & Annotations & Requires annotating sequences of valid cryptographic function calls\\
+ \CWE{327}: Use of a Broken or Risky Cryptographic Algorithm & Annotations & Requires annotating which algorithms are ``broken or risky''\\
+ \CWE{328}: Reversible One-Way Hash & Annotations & Requires annotating hash-related functions and variables\\
+ \CWE{338}: Use of Cryptographically Weak Pseudo-Random Number Generator (PRNG) & Annotations & Requires annotating PRNG-related functions and variables\\
+ \CWE{364}: Signal Handler Race Condition & Not Handled & -\\
+ \CWE{366}: Race Condition Within Thread & Not Handled & Some situations can be handled by the Mthread plugin\\
+ \CWE{367}: TOC TOU & Not Handled & -\\
+ \CWE{369}: Divide by Zero & Handled & -\\
+ \CWE{377}: Insecure Temporary File & Annotations & Requires annotating functions and data flows related to temporary files\\
+ \CWE{390}: Error Without Action & Not Handled & -\\
+ \CWE{391}: Unchecked Error Condition & Not Handled & -\\
+ \CWE{400}: Uncontrolled Resource Consumption & Annotations & Requires annotating resource-related functions and variables\\
+ \CWE{401}: Missing Release of Memory after Effective Lifetime & Not Handled & -\\
+ \CWE{404}: Improper Resource Shutdown or Release & Annotations & Requires annotating resources and functions manipulating them\\
+ \CWE{415}: Double Free & Handled & -\\
+ \CWE{416}: Use After Free & Handled & -\\
+ \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}\\
+ \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 & -\\
+ \CWE{468}: Incorrect Pointer Scaling & Syntactic & -\\
+ \CWE{469}: Use of Pointer Subtraction to Determine Size & Handled & -\\
+ \CWE{475}: Undefined Behavior for Input to API & Too Vague & \FramaC already handles some cases related to the C standard library, but in general, may require annotations\\
+ \CWE{476}: NULL Pointer Dereference & Handled & -\\
+ \CWE{478}: Missing Default Case in Switch & Syntactic & -\\
+ \CWE{479}: Signal Handler Use of Non Reentrant Function & Not Handled & -\\
+ \CWE{480}: Use of Incorrect Operator & Too Vague & -\\
+ \CWE{481}: Assigning Instead of Comparing & Syntactic & -\\
+ \CWE{482}: Comparing Instead of Assigning & Syntactic & -\\
+ \CWE{483}: Incorrect Block Delimitation & Syntactic & -\\
+ \CWE{484}: Omitted Break Statement in Switch & Syntactic & -\\
+ \CWE{506}: Embedded Malicious Code & Too Vague & Defining ``malicious code'' automatically is hard; manual annotations defeat the purpose\\
+ \CWE{510}: Trapdoor & Too Vague & Sound analyses such as those proposed by \FramaC are able to exhaustively identify some kinds of trapdoors\\
+ \CWE{511}: Logic/Time Bomb & Not Handled & -\\
+ \CWE{526}: Exposure of Sensitive Information Through Environmental Variables & Annotations & Requires annotating sensitive information and environment-related functions and variables\\
+ \CWE{546}: Suspicious Comment & Syntactic & -\\
+ \CWE{561}: Dead Code & Partially Handled & Metrics and Eva provide information about syntactic and semantic coverage\\
+ \CWE{562}: Return of Stack Variable Address & Handled & Related to Eva's warning category \texttt{locals-escaping}\\
+ \CWE{563}: Unused Variable & Syntactic & Mostly syntactic in nature; compilers often warn about it\\
+ \CWE{570}: Expression Always False & Syntactic & Mostly syntactic in nature; compilers often warn about it\\
+ \CWE{571}: Expression Always True & Syntactic & Mostly syntactic in nature; compilers often warn about it\\
+ \CWE{587}: Assignment of Fixed Address to Pointer & Handled & Detected via \texttt{-warn-invalid-pointer} at the assignment, otherwise indirectly at the point of usage; option \texttt{-absolute-valid-range} changes its behavior\\
+ \CWE{588}: Attempt to Access Child of a Non-structure Pointer & Partially Handled & \FramaC emits warnings for certain types of incompatible casts\\
+ \CWE{590}: Free Memory Not on Heap & Handled & -\\
+ \CWE{591}: Sensitive Data Storage in Improperly Locked Memory & Not Handled & -\\
+ \CWE{605}: Multiple Binds to the Same Port & Annotations & Requires annotating socket-related functions and variables\\
+ \CWE{606}: Unchecked Loop Condition & Annotations & Requires annotating which data is user-supplied\\
+ \CWE{615}: Inclusion of Sensitive Information in Source Code Comments & Not Handled & -\\
+ \CWE{617}: Reachable Assertion & Handled & \FramaC's libc \texttt{assert} specification contains an ACSL assertion\\
+ \CWE{620}: Unverified Password Change & Not Handled & -\\
+ \CWE{665}: Improper Initialization & Handled & -\\
+ \CWE{666}: Operation on Resource in Wrong Phase of Lifetime & Annotations & Requires annotating resources and their lifecycles\\
+ \CWE{667}: Improper Locking & Annotations & Requires annotating locks and functions manipulating them\\
+ \CWE{672}: Operation on Resource After Expiration or Release & Annotations & Requires annotating resources and their lifecycles\\
+ \CWE{674}: Uncontrolled Recursion & Too Vague & The identification of an ``uncontrolled'' recursion is complex\\
+ \CWE{675}: Duplicate Operations on Resource & Annotations & Requires annotating resources and operations on them\\
+ \CWE{676}: Use of Potentially Dangerous Function & Annotations & Requires annotating which functions are ``potentially dangerous''\\
+ \CWE{680}: Integer Overflow to Buffer Overflow & Handled & -\\
+ \CWE{681}: Incorrect Conversion Between Numeric Types & Partially Handled & See note about {\em Numerical Conversions}\\
+ \CWE{685}: Function Call With Incorrect Number of Arguments & Partially Handled & The Variadic plugin handles most cases related to variadic function calls\\
+ \CWE{688}: Function Call With Incorrect Variable or Reference as Argument & Partially Handled & Some cases are related to variadic functions (e.g. \texttt{printf}) and detected by the Variadic plugin\\
+ \CWE{690}: Unchecked Return Value to NULL Pointer Dereference & Handled & For functions related to dynamically allocated memory, toggled via option \texttt{-eva-alloc-returns-null}\\
+ \CWE{758}: Undefined Behavior & Partially Handled & The C language has too many undefined behaviors, but Frama-C does handle several of them\\
+ \CWE{761}: Free Pointer Not at Start of Buffer & Handled & -\\
+ \CWE{762}: Mismatched Memory Management Routines & Annotations & Requires annotating memory management functions and objects\\
+ \CWE{773}: Missing Reference to Active File Descriptor or Handle & Annotations & Requires annotating resources and operations on them\\
+ \CWE{775}: Missing Release of File Descriptor or Handle & Annotations & Requires annotating resources and their lifecycles\\
+ \CWE{780}: Use of RSA Algorithm Without OAEP & Not Handled & -\\
+ \CWE{785}: Path Manipulation Function Without Max Sized Buffer & Annotations & Requires all relevant filepath-related functions to have correct annotations\\
+ \CWE{786}: Access of Memory Location Before Start of Buffer & Handled & -\\
+ \CWE{787}: Out-of-bounds Write & Handled & -\\
+ \CWE{788}: Access of Memory Location After End of Buffer & Handled & -\\
+ \CWE{789}: Memory Allocation with Excessive Size Value & Annotations & Requires annotating memory limits\\
+ \CWE{823}: Use of Out-of-range Pointer Offset & Handled & -\\
+ \CWE{824}: Access of Uninitialized Pointer & Handled & -\\
+ \CWE{825}: Expired Pointer Dereference & Handled & -\\
+ \CWE{832}: Unlock of Resource That is Not Locked & Annotations & Requires annotating resources and operations on them\\
+ \CWE{835}: Infinite Loop & Partially Handled & Loops which, semantically, are {\em always} infinite are reported by the Nonterm plugin\\
+ \CWE{843}: Access of Resource Using Incompatible Type ('Type Confusion') & Not Handled & -\\
+ \CWE{912}: Hidden Functionality & Too Vague & \FramaC's sound analysis can show the absence of backdoors, but only if they can be semantically specified (e.g. via annotations)\\
+\end{longtable}
+}
+
+\paragraph{Note about {\em Numerical Conversions}}
+
+A few CWEs (\CWE{194}, \CWE{195}, \CWE{196} and \CWE{197}) related to numerical
+conversion issues do not map directly to undefined behaviors
+(except, in some cases, to {\em CC.36});
+some of them are related to unspecified and implementation-defined behaviors.
+\FramaC has a set of command-line options to enable warnings related to these
+conversions, when they can overflow or generate unexpected values:
+\texttt{-warn-signed-overflow}, \texttt{-warn-unsigned-overflow},
+\texttt{-warn-signed-downcast}, and \texttt{-warn-unsigned-downcast}.
+
+See Section~\ref{sec:customizing-analyzers} for more details and some examples
+related to these options.
+
+Also note that conversion from a floating-point value to an integer may
+overflow; in this case, an alarm \texttt{float\_to\_int} is generated,
+independently of the previous options.
+
+% Undoing the macros used by the tables in this chapter
+% restore longtables
+\renewenvironment{longtable}{\oldlongtable} {
+\endoldlongtable}
diff --git a/doc/userman/user-intro.tex b/doc/userman/user-intro.tex
index eaaf0c0a778922a5bc1aebfb860b67e9c2ac0d1d..9f60b97c9197c4208b4f690e71ef654599a68526 100644
--- a/doc/userman/user-intro.tex
+++ b/doc/userman/user-intro.tex
@@ -11,8 +11,8 @@ This manual gives an overview of \FramaC for newcomers,
and serves as a reference for expert users.
It only describes those platform features that are common to all analyzers.
Thus it \emph{does not cover} the use of the analyzers provided in the \FramaC
-distribution (Value Analysis, Slicing, \ldots). Each of these analyses has its
-own specific documentation~\cite{wp,value,rte,aorai}. Furthermore, research
+distribution (Eva, WP, E-ACSL, \ldots). Each of these analyses has its
+own specific documentation~\cite{wp,value,eacsl}. Furthermore, research
papers~\cite{sefm12,fac15} give a synthetic view of the platform, its main and
composite analyses, and some of its industrial achievements, while the
development of new analyzers is described in the Plug-in Development
@@ -60,6 +60,8 @@ The remainder of this manual is organized in several chapters.
as \texttt{printf} and \texttt{scanf}.
\item[Chapter~\ref{user-analysis-scripts}] details several scripts used to
help setup and run analyses on large code bases.
+\item[Chapter~\ref{user-compliance}] contains information related to compliance
+ to standards and coding guidelines (ISO C, CERT, CWEs, etc).
\item[Chapter~\ref{user-errors}] explains how to report errors \via \FramaC's
public Gitlab repository.
\end{description}
diff --git a/doc/userman/userman.bib b/doc/userman/userman.bib
index 5f1f3daa186874645e4d746fd06235c4c6781484..c696fc296452139addb6af4745d7c31fa0f41551 100644
--- a/doc/userman/userman.bib
+++ b/doc/userman/userman.bib
@@ -16,22 +16,22 @@
}
@manual{acsl,
- author = {Baudin, Patrick and Filli\^{a}tre, Jean-Christophe and
+ author = {Baudin, Patrick and Cuoq, Pascal and Filli\^{a}tre, Jean-Christophe and
March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
Prevosto, Virgile},
- month = mar,
- title = {{ACSL: ANSI/ISO C Specification Language. Version 1.8}},
- year = {2014}
+ month = nov,
+ title = {{ACSL: ANSI/ISO C Specification Language. Version 1.16}},
+ year = {2020}
}
@manual{acsl-implem,
- author = {Baudin, Patrick and Pascal Cuoq and Filli\^{a}tre, Jean-Christophe
- and March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
+ author = {Baudin, Patrick and Cuoq, Pascal and Filli\^{a}tre, Jean-Christophe and
+ March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
Prevosto, Virgile},
- month = mar,
- title = {ACSL: ANSI/ISO C Specification Language. Version 1.8 ---
- Frama-C Oxygen implementation.},
- year = {2014}
+ month = nov,
+ title = {ACSL: ANSI/ISO C Specification Language. Version 1.16 -- as implemented
+ in Frama-C 22.0},
+ year = {2020}
}
@misc{slicing,
@@ -84,7 +84,7 @@
@article{fac15,
year={2015},
journal={Formal Aspects of Computing},
-title={Frama-C: A software analysis perspective},
+title={{Frama-C}: A software analysis perspective},
publisher={Springer London},
keywords={Formal verification; Static analysis; Dynamic analysis; C},
author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
diff --git a/doc/userman/userman.tex b/doc/userman/userman.tex
index f78664bfc948f7e5908c1149f94756b2e8560e2b..bae73751949358cd1ed3de20751658cbbde76b83 100644
--- a/doc/userman/userman.tex
+++ b/doc/userman/userman.tex
@@ -3,6 +3,9 @@
\usepackage{graphicx}
\usepackage{calc}
+\usepackage{array}
+\usepackage{longtable}
+\usepackage{hyperref}
\include{macros}
\input{./frama-c-affiliation.tex}
@@ -27,10 +30,7 @@
\end{tabular}
\vfill
\begin{flushleft}
- \textcopyright 2009-2020 CEA LIST
-
-This work has been supported by the ANR project CAT (ANR-05-RNTL-00301) and by
-the ANR project U3CAT (08-SEGI-021-01).
+ \textcopyright 2009-2021 CEA LIST
\end{flushleft}
\end{titlepage}
@@ -43,15 +43,18 @@ the ANR project U3CAT (08-SEGI-021-01).
\addcontentsline{toc}{chapter}{Foreword}
This is the user manual of \FramaC\footnote{\url{http://frama-c.com}}. The
-content of this document corresponds to the version \framacversion (\today) of
-\FramaC. However the development of \FramaC is still ongoing: features
-described here may still evolve in the future.
+content of this document corresponds to the version \framacversion, on \today, of
+\FramaC.
\section*{Acknowledgements}
We gratefully thank all the people who contributed to this document: Patrick
Baudin, Mickaël Delahaye, Philippe Hermann, Benjamin Monate and Dillon Pariente.
+\acknowledgeANR
+
+\acknowledgeEU
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\include{user-intro}
@@ -66,6 +69,7 @@ Baudin, Mickaël Delahaye, Philippe Hermann, Benjamin Monate and Dillon Pariente
\include{user-report}
\include{user-variadic}
\include{user-analysis-scripts}
+\include{user-compliance}
\include{user-errors}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/doc/value/.gitignore b/doc/value/.gitignore
index a15bb914b73364a99358ebb658fc07b6832ca571..4cb469371c39fba5dc990341e237f39aab91592c 100644
--- a/doc/value/.gitignore
+++ b/doc/value/.gitignore
@@ -1,3 +1,5 @@
+/anr-logo.png
+/eu-flag.jpg
/frama-c-book.cls
/frama-c-cover.pdf
/frama-c-left.pdf
diff --git a/tests/value/invalid_pointer.c b/tests/value/invalid_pointer.c
index 09d7babf80b362a87d2dbe5971abb916271f240a..ba139caabda56485661900e92b37a4fba1f03155 100644
--- a/tests/value/invalid_pointer.c
+++ b/tests/value/invalid_pointer.c
@@ -167,6 +167,24 @@ void object_pointer_predicate () {
}
}
+/* CERT C UB 62. An attempt is made to access, or generate a pointer to just
+ past, a flexible array member of a structure when the referenced object
+ provides no elements for that array (6.7.2.1). */
+struct sfam {
+ int len;
+ char fam[];
+};
+
+void flexible_array_member() {
+ struct sfam s1 = { 0 };
+ if (undet) {
+ char *p = s1.fam + 1; // UB 62 (generate a pointer ...)
+ }
+ if (undet) {
+ char *p = s1.fam;
+ *(p+1) = 0; // UB 62 (access a pointer ...)
+ }
+}
void main () {
pointer_computation ();
@@ -176,6 +194,7 @@ void main () {
union_pointer ();
write_pointer ();
object_pointer_predicate ();
+ flexible_array_member();
// should not emit an alarm
signal (SIGUSR1, SIG_IGN);
signal (SIGUSR2, SIG_ERR);
diff --git a/tests/value/oracle/invalid_pointer.0.res.oracle b/tests/value/oracle/invalid_pointer.0.res.oracle
index 49074590ec4ff2071112e1ba7cdd78a2ff5f864e..4ac7d19881b6d1265648be10fb7439eaabc30516 100644
--- a/tests/value/oracle/invalid_pointer.0.res.oracle
+++ b/tests/value/oracle/invalid_pointer.0.res.oracle
@@ -8,7 +8,7 @@
NULL[rbits 80 to 247] ∈ [--..--]
undet ∈ [--..--]
[eva] computing for function pointer_computation <- main.
- Called from tests/value/invalid_pointer.c:172.
+ Called from tests/value/invalid_pointer.c:190.
[eva:alarm] tests/value/invalid_pointer.c:20: Warning:
invalid pointer creation. assert \object_pointer(p - 1);
[eva:alarm] tests/value/invalid_pointer.c:23: Warning:
@@ -37,7 +37,7 @@
[eva] Recording results for pointer_computation
[eva] Done for function pointer_computation
[eva] computing for function pointer_in_loops <- main.
- Called from tests/value/invalid_pointer.c:173.
+ Called from tests/value/invalid_pointer.c:191.
[eva] tests/value/invalid_pointer.c:43:
Trace partitioning superposing up to 100 states
[eva:alarm] tests/value/invalid_pointer.c:52: Warning:
@@ -45,7 +45,7 @@
[eva] Recording results for pointer_in_loops
[eva] Done for function pointer_in_loops
[eva] computing for function int_conversion <- main.
- Called from tests/value/invalid_pointer.c:174.
+ Called from tests/value/invalid_pointer.c:192.
[eva:alarm] tests/value/invalid_pointer.c:64: Warning:
invalid pointer creation. assert \object_pointer((int *)42);
[eva] computing for function Frama_C_interval <- int_conversion <- main.
@@ -72,7 +72,7 @@
[eva] Recording results for int_conversion
[eva] Done for function int_conversion
[eva] computing for function addrof <- main.
- Called from tests/value/invalid_pointer.c:175.
+ Called from tests/value/invalid_pointer.c:193.
[eva:alarm] tests/value/invalid_pointer.c:82: Warning:
invalid pointer creation. assert \object_pointer(&a[11]);
[eva:alarm] tests/value/invalid_pointer.c:84: Warning:
@@ -82,7 +82,7 @@
[eva] Recording results for addrof
[eva] Done for function addrof
[eva] computing for function union_pointer <- main.
- Called from tests/value/invalid_pointer.c:176.
+ Called from tests/value/invalid_pointer.c:194.
[eva:alarm] tests/value/invalid_pointer.c:102: Warning:
invalid pointer creation. assert \object_pointer(u.pointer);
[eva:alarm] tests/value/invalid_pointer.c:105: Warning:
@@ -90,7 +90,7 @@
[eva] Recording results for union_pointer
[eva] Done for function union_pointer
[eva] computing for function write_pointer <- main.
- Called from tests/value/invalid_pointer.c:177.
+ Called from tests/value/invalid_pointer.c:195.
[eva:alarm] tests/value/invalid_pointer.c:115: Warning:
invalid pointer creation. assert \object_pointer(p);
[eva:alarm] tests/value/invalid_pointer.c:118: Warning:
@@ -98,7 +98,7 @@
[eva] Recording results for write_pointer
[eva] Done for function write_pointer
[eva] computing for function object_pointer_predicate <- main.
- Called from tests/value/invalid_pointer.c:178.
+ Called from tests/value/invalid_pointer.c:196.
[eva] tests/value/invalid_pointer.c:127: assertion got status valid.
[eva:alarm] tests/value/invalid_pointer.c:129: Warning:
invalid pointer creation. assert \object_pointer(p - 1);
@@ -150,15 +150,25 @@
invalid pointer creation. assert \object_pointer((int *)100);
[eva] Recording results for object_pointer_predicate
[eva] Done for function object_pointer_predicate
+[eva] computing for function flexible_array_member <- main.
+ Called from tests/value/invalid_pointer.c:197.
+[eva:alarm] tests/value/invalid_pointer.c:181: Warning:
+ invalid pointer creation. assert \object_pointer(&s1.fam[1]);
+[eva:alarm] tests/value/invalid_pointer.c:185: Warning:
+ invalid pointer creation. assert \object_pointer(p_0 + 1);
+[kernel] tests/value/invalid_pointer.c:185: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva] Recording results for flexible_array_member
+[eva] Done for function flexible_array_member
[eva] computing for function signal <- main.
- Called from tests/value/invalid_pointer.c:180.
+ Called from tests/value/invalid_pointer.c:199.
[eva] using specification for function signal
[eva] Done for function signal
[eva] computing for function signal <- main.
- Called from tests/value/invalid_pointer.c:181.
+ Called from tests/value/invalid_pointer.c:200.
[eva] Done for function signal
[eva] computing for function signal <- main.
- Called from tests/value/invalid_pointer.c:182.
+ Called from tests/value/invalid_pointer.c:201.
[eva] Done for function signal
[eva] Recording results for main
[eva] done for function main
@@ -186,11 +196,17 @@
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:165:
assertion 'Eva,pointer_value' got final status invalid.
+[eva] tests/value/invalid_pointer.c:181:
+ assertion 'Eva,pointer_value' got final status invalid.
+[eva] tests/value/invalid_pointer.c:185:
+ assertion 'Eva,pointer_value' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function addrof:
p ∈ {{ &a + [0..40],0%4 }}
offset ∈ [--..--]
+[eva:final-states] Values at end of function flexible_array_member:
+ s1 ∈ {0}
[eva:final-states] Values at end of function int_conversion:
Frama_C_entropy_source ∈ [--..--]
x ∈ [15..31]
@@ -347,6 +363,8 @@
Frama_C_entropy_source ∈ [--..--]
[from] Computing for function addrof
[from] Done for function addrof
+[from] Computing for function flexible_array_member
+[from] Done for function flexible_array_member
[from] Computing for function int_conversion
[from] Computing for function Frama_C_interval <-int_conversion
[from] Done for function Frama_C_interval
@@ -372,6 +390,8 @@
\result FROM Frama_C_entropy_source; min; max
[from] Function addrof:
NO EFFECTS
+[from] Function flexible_array_member:
+ NO EFFECTS
[from] Function int_conversion:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function object_pointer_predicate:
@@ -393,6 +413,10 @@
p; offset
[inout] Inputs for function addrof:
undet
+[inout] Out (internal) for function flexible_array_member:
+ s1; p; p_0
+[inout] Inputs for function flexible_array_member:
+ undet
[inout] Out (internal) for function int_conversion:
Frama_C_entropy_source; x; p
[inout] Inputs for function int_conversion:
diff --git a/tests/value/oracle/invalid_pointer.1.res.oracle b/tests/value/oracle/invalid_pointer.1.res.oracle
index 132d1bef54df6c456d61b9acf25df882c73a6d48..4294f5e3507343b2e34a19ba1602a5672f9fc112 100644
--- a/tests/value/oracle/invalid_pointer.1.res.oracle
+++ b/tests/value/oracle/invalid_pointer.1.res.oracle
@@ -8,7 +8,7 @@
NULL[rbits 80 to 247] ∈ [--..--]
undet ∈ [--..--]
[eva] computing for function pointer_computation <- main.
- Called from tests/value/invalid_pointer.c:172.
+ Called from tests/value/invalid_pointer.c:190.
[eva] computing for function Frama_C_interval <- pointer_computation <- main.
Called from tests/value/invalid_pointer.c:31.
[eva] using specification for function Frama_C_interval
@@ -23,7 +23,7 @@
[eva] Recording results for pointer_computation
[eva] Done for function pointer_computation
[eva] computing for function pointer_in_loops <- main.
- Called from tests/value/invalid_pointer.c:173.
+ Called from tests/value/invalid_pointer.c:191.
[eva] tests/value/invalid_pointer.c:43:
Trace partitioning superposing up to 100 states
[eva] tests/value/invalid_pointer.c:54:
@@ -31,7 +31,7 @@
[eva] Recording results for pointer_in_loops
[eva] Done for function pointer_in_loops
[eva] computing for function int_conversion <- main.
- Called from tests/value/invalid_pointer.c:174.
+ Called from tests/value/invalid_pointer.c:192.
[eva] computing for function Frama_C_interval <- int_conversion <- main.
Called from tests/value/invalid_pointer.c:66.
[eva] tests/value/invalid_pointer.c:66:
@@ -50,19 +50,19 @@
[eva] Recording results for int_conversion
[eva] Done for function int_conversion
[eva] computing for function addrof <- main.
- Called from tests/value/invalid_pointer.c:175.
+ Called from tests/value/invalid_pointer.c:193.
[eva] Recording results for addrof
[eva] Done for function addrof
[eva] computing for function union_pointer <- main.
- Called from tests/value/invalid_pointer.c:176.
+ Called from tests/value/invalid_pointer.c:194.
[eva] Recording results for union_pointer
[eva] Done for function union_pointer
[eva] computing for function write_pointer <- main.
- Called from tests/value/invalid_pointer.c:177.
+ Called from tests/value/invalid_pointer.c:195.
[eva] Recording results for write_pointer
[eva] Done for function write_pointer
[eva] computing for function object_pointer_predicate <- main.
- Called from tests/value/invalid_pointer.c:178.
+ Called from tests/value/invalid_pointer.c:196.
[eva] tests/value/invalid_pointer.c:127: assertion got status valid.
[eva:alarm] tests/value/invalid_pointer.c:130: Warning:
assertion got status invalid (stopping propagation).
@@ -103,23 +103,35 @@
assertion got status invalid (stopping propagation).
[eva] Recording results for object_pointer_predicate
[eva] Done for function object_pointer_predicate
+[eva] computing for function flexible_array_member <- main.
+ Called from tests/value/invalid_pointer.c:197.
+[eva:alarm] tests/value/invalid_pointer.c:185: Warning:
+ out of bounds write. assert \valid(p_0 + 1);
+[kernel] tests/value/invalid_pointer.c:185: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva] Recording results for flexible_array_member
+[eva] Done for function flexible_array_member
[eva] computing for function signal <- main.
- Called from tests/value/invalid_pointer.c:180.
+ Called from tests/value/invalid_pointer.c:199.
[eva] using specification for function signal
[eva] Done for function signal
[eva] computing for function signal <- main.
- Called from tests/value/invalid_pointer.c:181.
+ Called from tests/value/invalid_pointer.c:200.
[eva] Done for function signal
[eva] computing for function signal <- main.
- Called from tests/value/invalid_pointer.c:182.
+ Called from tests/value/invalid_pointer.c:201.
[eva] Done for function signal
[eva] Recording results for main
[eva] done for function main
+[eva] tests/value/invalid_pointer.c:185:
+ assertion 'Eva,mem_access' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function addrof:
p ∈ {{ &a + [-8589934592..8589934588],0%4 }}
offset ∈ [--..--]
+[eva:final-states] Values at end of function flexible_array_member:
+ s1 ∈ {0}
[eva:final-states] Values at end of function int_conversion:
Frama_C_entropy_source ∈ [--..--]
x ∈ [15..100]
@@ -275,6 +287,8 @@
Frama_C_entropy_source ∈ [--..--]
[from] Computing for function addrof
[from] Done for function addrof
+[from] Computing for function flexible_array_member
+[from] Done for function flexible_array_member
[from] Computing for function int_conversion
[from] Computing for function Frama_C_interval <-int_conversion
[from] Done for function Frama_C_interval
@@ -300,6 +314,8 @@
\result FROM Frama_C_entropy_source; min; max
[from] Function addrof:
NO EFFECTS
+[from] Function flexible_array_member:
+ NO EFFECTS
[from] Function int_conversion:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function object_pointer_predicate:
@@ -321,6 +337,10 @@
p; offset
[inout] Inputs for function addrof:
undet
+[inout] Out (internal) for function flexible_array_member:
+ s1; p; p_0
+[inout] Inputs for function flexible_array_member:
+ undet
[inout] Out (internal) for function int_conversion:
Frama_C_entropy_source; x; p
[inout] Inputs for function int_conversion: