--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] linked lists?



Hello,

On 30/11/2011 20:42, Stephen Siegel wrote:
> Hi, I was trying to do something with this example taken from one of
> the ACSL manuals, but got an unimplemented feature error. I'm still
> using Carbon release.

> /*@
>    requires reachable(p,\null);
>    assigns { q->hd | struct list *q ; reachable(p,q) } ;
>    @*/

I havn't looked at it in very detail, but it is most probably the 
assigns clause that's causing trouble here. Comprehension (i.e. the 
possibility of considering the set of all q->hd such that reachable(p,q) 
is supported by the front-end, but not by any plug-in I know of. I'm 
afraid Frama-C Nitrogen won't help in this particular case.

There have been few attempts to study  such structures so far, but I 
have to admit that it is not the main topic of most usages of Frama-C.

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