@@ -303,7 +303,6 @@ them to generate efficient proof obligations.
% replaces the \texttt{Store} one; the \texttt{Runtime} model will be entirely
% re-implemented as \texttt{Bytes} model in some future release.
\clearpage
\section{Arithmetic Models}
\label{wp-model-arith}
...
...
@@ -346,7 +345,7 @@ For tackling this complexity, the \textsf{WP} plug-in relies on several
\item[Float Model:] floating-point values are represent in a special
theory with dedicated operations over \texttt{float} and \texttt{double}
values and conversion from and to their \texttt{real} representation \emph{via}
rounding, as defined by the \textsc{C/ACSL} semantics.
rounding, as defined by the \textsf{C/ACSL} semantics.
Although correct with respect to the \textsc{IEEE} specifications, this
model still provides very little support for proving properties with automated
...
...
@@ -365,4 +364,71 @@ For tackling this complexity, the \textsf{WP} plug-in relies on several
proofs to be correct. Depending on the model used and the kernel options, those conditions
may change. WP do not generate proof obligations for runtime errors on its own. Instead, it can
discharge the annotations generated by the \textsf{Eva} analysis plug-in, or by the \textsf{RTE} plug-in.
Consider also using \textsf{-wp-rte} option.
Consider also using \texttt{-wp-rte} option.
\section{Limitations, Roadmap}
The ambition of \textsf{WP} plug-in is to cover as many \textsf{ACSL} features as possible. However, some of them are still not available yet, because of lack of manpower or more fundamental reasons. This section provides an overview of those limitations, with roadmap indications: \textit{easy}
means that support could be provided on demand, \textit{medium} means that
significant manpower is required to implement the feature and \textit{hard} means that a mid-term research project would be required. This list of limitations is probably not exhaustive (yet) and will be maintained over future versions of \textsf{Frama-C/WP}.
\begin{description}
\item[Global Invariants.]
Not implemented yet (\textit{easy}).
\item[Type Invariants.]
Type invariants requires to be coupled with new memory models and
some memory region analysis (\textit{hard}).
\item[Model Fields.]
This \textsf{ACSL} feature is generally coupled with type invariants and global invariants, hence it is not implemented yet. From a practical point
of view, we think that ghost fields with logic types would be very complementary and easier to use. We are waiting for challenging use cases
to implement these features (\textit{medium}).
\item[Statement Contracts.]
No more supported since \textsf{Frama-C 23} (Vanadium) because of
unsoundness bugs to be fixed and \textsf{ACSL} restrictions.
Support shall be restored on a mid-term basis (\textit{easy}).
\item[Non-natural Loops.]
Loop constructed with \textsf{goto} are no more supported since
\textsf{Frama-C 23} (Vanadium) because of unsoundness bugs to be fixed.
A new engine is under construction but is not yet ready (\textit{medium}).
\item[Dynamic Allocation.]
All implemented memory models \emph{are} able to deal with dynamic allocation,
which is actually used internally to manage the scope of local variables.
However, \textsf{ACSL} clauses for specifying allocation and deallocation
are not implemented yet (\textit{medium}).
\item[Termination.]
Verification of function termination is not implemented yet, although
the support of \textsf{ACSL}\texttt{loop variant} is implemented.
Full support for \texttt{terminates} clause could be easily provided
and coupled with the reachability analysis for dead-code smoke tests
(\textit{easy}).
\item[Assigns.]
The WP strategy for proving assign clauses is a based on a sound but incomplete verification: we check that side effects
(writes and called assigns) are \emph{included} in specified assigns, which
is a sufficient but not necessary condition. The known workaround is to
specify larger assigns and to add the missing equalities to contracts.
Indeed, looking for an efficient and more permissive strategy is challenging (\textit{hard}).
\item[Froms.]
Proving \textsf{ACSL} assigns-from clauses is not implemented. It is as difficult as proving functional assigns. Although, we have designed some
heuristics to prove assigns-from clauses in simple cases that could be implemented on a mid-term basis (\textit{medium}).
\item[Per-behavior Assigns.]
Different assigns clause associated with distinct behaviors are difficult to
take into account without a deep refactoring of the WP rule of calls. We currently use a sound upper-approximation of assigns for function calls that might make correct \textsf{ACSL} properties not provable by lack of precision
(\textit{medium}).
\item[Low level Memory Models.]
Memory models with non-typed access and bit or byte precision would be easy to implement, although terribly inefficient. We are currently working on a new
memory analysis that would provide a deep understanding of how to make
\emph{different} memory models soundly working with each others on distinct memory regions, although this is part of a long-term research plan founded by
various collaborative projects (\textit{hard}).
\item[IEEE Floats.]
A new sound but incomplete model for floats is provided since \textsf{Frama-C 21} (Scandium). Its incomplete nature makes it difficult to prove arithmetic
properties of float operations by lack of good support from \textsf{SMT} solvers. Although, recent advances on our \textsf{Colibri} solver open the road to a better support for float operations in a near future (\textit{medium}/\textit{hard}).
\item[Function Pointers.]
Limited support for function pointers is provided \emph{via} an extension of \textsf{ACSL}, see Section~\ref{acsl:calls} for details. Currently, a function
pointer must be provably equal to a finite list of known functions. Although,
this could be easily extended to support function contract refinement (\textit{medium}).
