--- layout: fc_discuss_archives title: Message 102 from Frama-C-discuss on January 2014 ---
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>