--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on November 2013 ---
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