--- layout: fc_discuss_archives title: Message 12 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,

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