--- layout: fc_discuss_archives title: Message 72 from Frama-C-discuss on December 2009 ---
hi, I try to use the jessie plug-in to verify a double list code. But I' ve met a problem and the error message is so simple that I can't fix the problem. I use Beryllium-20090902 with why version 2.23. Here is the code: --------------------------------------------------------------------------------------------------- /* the node of the list */ typedef struct ChainNode_Struct ChainNode; struct ChainNode_Struct { ChainNode *next; ChainNode *previous; }; /* definition of the head of the list */ typedef struct { ChainNode *head; ChainNode *null; ChainNode *tail; } ChainControl; /* get the head */ /*@ requires \valid(chain) && chain != NULL; ensures \result != NULL; */ ChainNode *_ChainHead( ChainControl *chain ) { return (ChainNode *) chain; } /* get the tail */ /*@ requires \valid(chain) && chain != NULL; ensures \result != NULL; */ ChainNode *_ChainTail( ChainControl *chain ) { return (ChainNode *) &chain->null; } /* check if the list is empty */ /*@ requires \valid(the_chain) && the_chain != NULL; ensures (the_chain -> head == the_chain + sizeof(ChainNode*)) ? \result == true : \result == false; */ T_UWORD ChainIsEmpty( ChainControl *the_chain ) { return ( the_chain->head == _ChainTail( the_chain ) ); } /* initialize the list */ /*@ requires \valid(the_chain) && the_chain != NULL; ensures (the_chain -> head == the_chain + sizeof(ChainNode*)) && (the_chain -> tail == the_chain) && (the_chain -> NULL == NULL); */ void InitializeChain( ChainControl *chain ) { chain->head = _ChainTail( chain ); chain->null = NULL; chain->tail = _ChainHead( chain ); } ------------------------------------------------------------------------------------------------- The error message is : ------------------------------------------------------------------------------------------------- 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 [kernel] user error: skipping file "./list.c" that has errors. [kernel] Plugin kernel aborted because of invalid user input(s). ------------------------------------------------------------------------------------------------- Could any one tell me how to make it to show more error message(I've tried -verbose 2, but it gave the information I do not need.) and help me to fix the error of the code above.Thanks! Best Regards, Chen -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091208/17f2cb45/attachment.htm