--- layout: fc_discuss_archives title: Message 124 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



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