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

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