Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about axiomatic and type invariant

Hello,

2015-01-30 9:58 GMT+01:00 Wong Ford Long <wfordlon at dso.org.sg>:

> [wp] warning: No definition for 'length' interpreted as reads nothing
>
> How should this message be understood?
> Has something above been written wrongly, causing 'length' to be undefined?
> How to correct this, so that 'length' can be used in the annotation
> of some function that manipulates the struct 'list'?
>

The definition of length is correct with respect to ACSL. However, the
WP plugin requires that all functions or predicates that are defined
axiomatically must have a 'reads' clause. The issue here is that the
reads clause is quite complicated, since we have to follow all nodes
from l:

 logic integer length{L}(list* l) reads { *node | list* node;
reachable(l,node) };

is the correct ACSL syntax for that, but I won't bet that WP will
understand much of it.

>
> Regarding
> function2.c:17:[wp] warning: Type invariant not handled yet ('finite_list'
> ignored)
>
> Does the Neon version (ver 20140301) of Frama-C handle such type invariant?
> Or would future versions do so?

As far as I know, there is not short-term plan of doing that in WP.
Note that on small development you can of course replace the type
invariant by explicit requires and ensures clauses.
In addition, this part of the tutorial (which by the way is largely
outdated, you might want to have a look at Fraunhofer FOKUS' ACSL By
Example
http://www.fokus.fraunhofer.de/download/acsl_by_example) was mainly
here to show an example of specification. I'm afraid that trying to
perform verification with WP on linked lists will require a big amount
of effort.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile