--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on January 2015 ---
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