--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on November 2011 ---
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. Does anyone understand what the feature is that's missing? Could this example work in Nitrogen release? Does anyone know any examples applying Frama-C to dynamic data structures such as linked lists? Thx, Steve struct list { int hd; struct list *next; }; /*@ inductive reachable{L}(struct list *root, struct list *to) { case empty{L}: \forall struct list *l; reachable(l,l) ; case non_empty{L}: \forall struct list *l1,*l2; \valid(l1) && reachable(l1->next,l2) ==> reachable(l1,l2) ; } @*/ // The requires clause forbids to give a circular list /*@ requires reachable(p,\null); assigns { q->hd | struct list *q ; reachable(p,q) } ; @*/ void incr_list(struct list *p) { while (p) { p->hd++ ; p = p->next; } } list$ frama-c -jessie list.c [kernel] preprocessing with "gcc -C -E -I. -dD list.c" [jessie] Starting Jessie translation [kernel] State_builder.aborted because of unimplemented feature. Please send a feature request at http://bts.frama-c.com with: 'Interp.terms Tcomprehension'. list$