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] Frama-c: WP issues with Alt-Ergo (but works with Z3)

  • Subject: [Frama-c-discuss] Frama-c: WP issues with Alt-Ergo (but works with Z3)
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Sun, 16 Feb 2014 16:01:57 -0500
  • In-reply-to: <52D6B7B0.4020005@fr.merce.mee.com>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C76682DC29@Mail1.FCMD.local>, <52D6B7B0.4020005@fr.merce.mee.com>
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>