--- layout: fc_discuss_archives title: Message 72 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problem with verify a list



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