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] Application to list_head_prev_0_new_0_4 creates an alias

  • Subject: [Frama-c-discuss] Application to list_head_prev_0_new_0_4 creates an alias
  • From: khoroshilov at ispras.ru (Alexey Khoroshilov)
  • Date: Fri, 26 Nov 2010 17:23:10 +0300
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>