--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on October 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problem with an example in acsl 1.4 doc



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