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

[Frama-c-discuss] Frama-c: WP issues with Alt-Ergo (but works with Z3)



Hi,

For the attached program, all the properties were proved by Z3 but Alt-Ergo timeout/Unknown for loop invariants.

If I replace UINT_MAX by a small constant, say 100, then Alt-Ergo was also able to prove if I substitute UINT_MAX by 1000.

Is there any possibility to make this program verifiable with Alt-Ergo?

Here is my log for Z3 and Alt-Ergo:


[formal_verification]$ frama-c -wp -wp-rte  -pp-annot -wp-timeout 25 -wp-proof=z3 c_nullify.c 
[kernel] preprocessing with "gcc -C -E -I.  -dD c_nullify.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function C_nullify
[rte] annotating function main
[wp] 13 goals scheduled
[wp] [Qed] Goal typed_C_nullify_loop_inv_established : Valid
[wp] [Qed] Goal typed_C_nullify_loop_assign_part1 : Valid
[wp] [Z3] Goal typed_C_nullify_assert_rte_unsigned_overflow : Valid (10ms)
[wp] [Z3] Goal typed_C_nullify_assert_rte_mem_access : Valid (10ms)
[wp] [Z3] Goal typed_C_nullify_loop_inv_preserved : Valid (10ms)
[wp] [Z3] Goal typed_C_nullify_loop_assign_part2 : Valid (10ms)
[wp] [Qed] Goal typed_C_nullify_assign_part1 : Valid
[wp] [Qed] Goal typed_C_nullify_loop_term_decrease : Valid
[wp] [Qed] Goal typed_C_nullify_loop_term_positive : Valid
[wp] [Qed] Goal typed_main_call_C_nullify_pre : Valid
[wp] [Qed] Goal typed_main_call_C_nullify_pre_2 : Valid
[wp] [Z3] Goal typed_C_nullify_assign_part2 : Valid
[wp] [Z3] Goal typed_C_nullify_loop_assign_part3 : Valid (20ms)



[formal_verification]$ frama-c -wp -wp-rte  -pp-annot -wp-timeout 100 -wp-proof=alt-ergo c_nullify.c 
[kernel] preprocessing with "gcc -C -E -I.  -dD c_nullify.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function C_nullify
[rte] annotating function main
[wp] 13 goals scheduled
[wp] [Qed] Goal typed_C_nullify_loop_inv_established : Valid
[wp] [Qed] Goal typed_C_nullify_loop_assign_part1 : Valid
[wp] [Alt-Ergo] Goal typed_C_nullify_assert_rte_unsigned_overflow : Valid (13)
[wp] [Alt-Ergo] Goal typed_C_nullify_assert_rte_mem_access : Valid (20ms) (22)
[wp] [Qed] Goal typed_C_nullify_assign_part1 : Valid
[wp] [Alt-Ergo] Goal typed_C_nullify_loop_assign_part2 : Valid (20ms) (23)
[wp] [Qed] Goal typed_C_nullify_loop_term_decrease : Valid
[wp] [Alt-Ergo] Goal typed_C_nullify_loop_assign_part3 : Valid (Qed:4ms) (24ms) (31)
[wp] [Qed] Goal typed_C_nullify_loop_term_positive : Valid
[wp] [Alt-Ergo] Goal typed_C_nullify_assign_part2 : Valid (16ms) (16)
[wp] [Qed] Goal typed_main_call_C_nullify_pre : Valid
[wp] [Qed] Goal typed_main_call_C_nullify_pre_2 : Valid
[wp] [Alt-Ergo] Goal typed_C_nullify_loop_inv_preserved : Unknown (Qed:4ms) (12s)



Thanks,
Dharma
-------------- next part --------------
A non-text attachment was scrubbed...
Name: c_nullify.c
Type: text/x-csrc
Size: 432 bytes
Desc: c_nullify.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140216/50f3e3e9/attachment.c>