--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on December 2011 ---
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