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

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