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



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.