--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on October 2009 ---
Thanks, my problem is solved. In my project I need to use jessie to generate the vc of coq. I think the out put of the error message is too brief to fix the error. Is there anyway to print a detailed error message? Best regards, Chen 2009/10/22 Anne Pacalet <anne.pacalet at sophia.inria.fr> > geng chen wrote : > > I've met a problem with the example in acsl 1.4 document. > > tang at tang-desktop:~/Desktop/bsearch$ frama-c -jessie ./bsearch.c > > [kernel] preprocessing with "gcc -C -E -I. -dD ./bsearch.c" > > ./bsearch.c:7:[kernel] user error: syntax error while parsing annotation > > It seems that it is only because at the end of the line : > @ behavior success: > you've put a ';' instead of a ':'... > > Notice that to test the syntaxe without calling any pluggin, > you can test with frama-c without any option. > > I cannot run the jessie plugin at the moment, > so I cannot check if it runs on your example. > > Hope this help anyway. > -- > Anne. > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091022/4621ac41/attachment.htm