--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP: Max_List syntax error



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>