--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] unable to interprete and trace jessie's output errors



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>