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] linked lists?

  • Subject: [Frama-c-discuss] linked lists?
  • From: siegel at udel.edu (Stephen Siegel)
  • Date: Wed, 30 Nov 2011 14:42:15 -0500
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$