--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on October 2009 ---
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.