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,

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