--- layout: fc_discuss_archives title: Message 106 from Frama-C-discuss on December 2009 ---
Hi, Le mar. 08 d?c. 2009 17:31:12 CET, geng chen <chengeng4001 at gmail.com> a ?crit : > tang at tang-desktop:~/Desktop/test_verify_SVMK$ frama-c -jessie ./list.c > [kernel] preprocessing with "gcc -C -E -I. -dD ./list.c" > ./list.c:24:[kernel] user error: syntax error There are at least two issues in your code, which will prevent its compilation with any C compiler: - T_UWORD is not defined (I suspect that's the complaint of Frama-C, but since your lines got wrapped, it's difficult to say) - neither is NULL I suspect you forgot to #include an header somewhere. In addition, your annotations needed some rewrite too - once NULL is defined, do not forget to add -pp-annot to command-line options of Frama-C. - there is a -> NULL which IMO should read -> null - you're comparing pointers of distinct types. In addition, you're doing pointer arithmetic in a way which looks quite suspicious. Casting everything to (char *) would probably help. - Built-ins \true and \false need their initial backslash ('\'). - NULL is never \valid, your preconditions are a bit redundant. Hope this helps, -- E tutto per oggi, a la prossima volta. Virgile