--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on November 2013 ---
Hello Virgile, I added label to the annotation: /*------------- code starts --------------*/ typedef struct dlnode { struct dlnode *next; struct dlnode *previous; } DL_NODE; /*@ inductive reachable{L} (DL_NODE* root, DL_NODE* node) { case root_reachable{L}: \forall DL_NODE* root; reachable(root,root); case next_reachable{L}: \forall DL_NODE* root, *node; \valid(root) ==> reachable(root->next, node) ==> reachable(root,node); } @*/ /*-----------------code ends -----------------*/ $ frama-c -jessie inductive_def.c $ why --coq inductive_def.why File "inductive_def.why", line 17, characters 29-35: Unbound type 'tag_id' I still got "unbound type" error. The file inductive_def.c just contains the code quoted above. Any ideas what goes wrong? Many thanks. xiaolei > Date: Mon, 4 Nov 2013 09:12:37 +0100 > From: virgile.prevosto at m4x.org > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] unable to interprete and trace jessie's output errors > > Hello, > > 2013/11/4 Xiao-lei Cui <x_cui at hotmail.com>: > > > /*@ > > inductive reachable (DL_NODE* root, DL_NODE* node) { > > case root_reachable: > > \forall DL_NODE* root; reachable(root,root); > > case next_reachable: > > \forall DL_NODE* root, *node; > > \valid(root) ==> reachable(root->next, node) ==> > > reachable(root,node); > > } > > @*/ > > > > However, I don't see errors from the quoted code above. Any ideas what > > went wrong? > > You should specify that reachable takes a logic label (e.g. {L}) as > argument. See the thread on "label L required?" for more information. > > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discu -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131104/80d4aa8d/attachment-0001.html>