Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] problem with verify a list
  • From: chengeng4001 at gmail.com (geng chen)
  • Date: Tue, 15 Dec 2009 14:58:18 +0800
  • In-reply-to: <20091210153736.0d036fe7@is010235>
  • References: <278036530912080131o202f8834xacf4b249c4b5b97@mail.gmail.com> <20091210153736.0d036fe7@is010235>
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