@@ -366,66 +366,64 @@ may change. WP do not generate proof obligations for runtime errors on its own.
discharge the annotations generated by the \textsf{Eva} analysis plug-in, or by the \textsf{RTE} plug-in.
Consider also using \texttt{-wp-rte} option.
\section{Limitations, Roadmap}
\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.]
\item[Global invariants.]
Not implemented yet (\textit{easy}).
\item[Type Invariants.]
\item[Type invariants.]
Type invariants requires to be coupled with new memory models and
some memory region analysis (\textit{hard}).
\item[Model Fields.]
\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.]
\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.]
\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.]
\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
the support of \textsf{ACSL}\texttt{loop variant} is provided.
Full support for \texttt{terminates} clause could be easily added
and combined with the reachability analysis of 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}).
Indeed, looking for an efficient and more permissive strategy would be 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.]
\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.]
\item[Bytes, unions \& casts.]
Memory models with non-typed access and bit- or byte-precision access 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. This would deserve a brand new research plan, to be founded by collaborative projects (\textit{hard}).
\item[Floats.]
A new sound but incomplete model for floats is provided since \textsf{Frama-C 21} (Scandium). Here, by incomplete we means that it is generally 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/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}).
pointer must be provably equal to a finite set of known functions. Although,
this could be easily extended to support function contracts refinement (\textit{medium}).
