--- layout: fc_discuss_archives title: Message 124 from Frama-C-discuss on December 2009 ---
Thanks for your help. But there are still some problems. And this time I only use a small piece of code. -------------------------------------------------------------------------------------- #ifndef NULL #define NULL 0 #endif typedef struct T_VMK_ChainNode_Struct T_VMK_ChainNode; struct T_VMK_ChainNode_Struct { T_VMK_ChainNode *next; T_VMK_ChainNode *previous; }; typedef struct { T_VMK_ChainNode *head; T_VMK_ChainNode *null; T_VMK_ChainNode *tail; } T_VMK_ChainControl; /*@ requires \valid(chain); ensures \result != NULL; */ VMK_INLINE T_VMK_ChainNode *_ChainHead( T_VMK_ChainControl *chain ) { return (T_VMK_ChainNode *) chain; } -------------------------------------------------------------------------------------- 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:28:[kernel] user error: syntax error [kernel] user error: skipping file "./list.c" that has errors. [kernel] Plugin kernel aborted because of invalid user input(s). --------------------------------------------------------------------------------------- Best Regards, Chen 2009/12/10 Virgile Prevosto <virgile.prevosto at cea.fr> > 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 > > > _______________________________________________ > 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/20091215/12ba7c73/attachment-0001.htm