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] 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>