--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Application to list_head_prev_0_new_0_4 creates an alias



Hi!

Could you please clarify what does the following error message mean?

 > frama-c -jessie -jessie-atp gui list.c
[kernel] preprocessing with "gcc -C -E -I.  -dD list.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir list.jessie
[jessie] File list.jessie/list.jc written.
[jessie] File list.jessie/list.cloc written.
[jessie] Calling Jessie tool in subdir list.jessie
Generating Why function __list_add
Generating Why function list_add
[jessie] Calling VCs generator.
gwhy-bin [...] why/list.why
Computation of VCs...
File "why/list.why", line 659, characters 87-111:
Application to list_head_prev_0_new_0_4 creates an alias
make: *** [list.stat] Error 1
[jessie] user error: Jessie subprocess failed: make -f list.makefile gui


The error message disappears if someone reduces assigns clause of 
__list_add or remove call of __list_add.

--
Regards,
Alexey Khoroshilov
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: khoroshilov at linuxtesting.org

-------------- next part --------------
A non-text attachment was scrubbed...
Name: list.c
Type: text/x-csrc
Size: 897 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101126/b703c7f7/attachment.c>