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] WP: Max_List syntax error

  • Subject: [Frama-c-discuss] WP: Max_List syntax error
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Thu, 30 Jan 2014 13:52:36 -0500
Hi,

I took the attached C program from the ACSL tutorial. Tried to apply it using WP but got  some errors.

Any suggestion?

Thanks,
Dharma

[formal_verification]$ frama-c -wp -wp-rte -lib-entry -main max_list max_list.c 
[kernel] preprocessing with "gcc -C -E -I.  max_list.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function max_list
max_list.c:35:[wp] warning: Ignored 'terminates' specification:
               finite(root)
max_list.c:33:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 7 goals scheduled
------------------------------------------------------------
--- Alt-Ergo (stderr) :
------------------------------------------------------------
File "/tmp/wp23d9ab.dir/typed/max_list_post_2_Alt-Ergo.mlw", line 216, characters 47-74:typing error: (addr,addr) farray and addr cannot be unified

------------------------------------------------------------
[wp] [Alt-Ergo] Goal typed_max_list_post_2 : Failed
     Error: Alt-Ergo exits with status [1]
------------------------------------------------------------
--- Alt-Ergo (stderr) :
------------------------------------------------------------
File "/tmp/wp23d9ab.dir/typed/max_list_post_Alt-Ergo.mlw", line 216, characters 47-74:typing error: (addr,addr) farray and addr cannot be unified

------------------------------------------------------------
[wp] [Alt-Ergo] Goal typed_max_list_assert_rte_mem_access_2 : Unknown
[wp] [Alt-Ergo] Goal typed_max_list_assert_rte_mem_access : Valid (16ms) (10)
[wp] [Alt-Ergo] Goal typed_max_list_post : Failed
     Error: Alt-Ergo exits with status [1]
[wp] [Qed] Goal typed_max_list_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_max_list_assert_rte_mem_access_5 : Valid
[wp] [Alt-Ergo] Goal typed_max_list_assert_rte_mem_access_4 : Unknown
[formal_verification]$ 




-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_list.c
Type: text/x-csrc
Size: 857 bytes
Desc: max_list.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140130/54ae7aaa/attachment.c>