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: mohamed.iguernelala at ocamlpro.com (Mohamed Iguernelala)
  • Date: Mon, 17 Feb 2014 07:42:21 +0100
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7BB59DEAB@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C76682DC29@Mail1.FCMD.local>, <52D6B7B0.4020005@fr.merce.mee.com> <B517F47C2F6D914AA8121201F9EBEE6701C7BB59DEAB@Mail1.FCMD.local>
Hello,

> Is there any possibility to make this program verifiable with Alt-Ergo?
Yes ... with option *-max-split -1*

More precisely, the decision procedure of linear integer arithmetic in 
Alt-Ergo uses bounds inference and interval calculus [1].
It is based on the following claims:
(a) If all the affine forms of the problem are unbounded, we are sure 
that this problem has a solution.
(b) If some affine form has a lower (integer) bound *L* and an upper 
bound *U*, Alt-Ergo may try all the possible integer values in [| L , 
U|] to see if there exists a solution that satisfies these bounds.

In practice, when the intervals *[| L , U|]* are huge, Alt-Ergo may 
spend a lot of time in (b), which makes it "unfair". So, we put a 
"max-split" limit in this part of Alt-Ergo to prevent it from 
"diverging". The option -max-split -1 deactivates this limit.

[1] A Simplex-Based Extension of Fourier-Motzkin for Solving Linear 
Integer Arithmetic: F. Bobot, S. Conchon, E. Contejean, M. Iguernelala, 
A. Mahboubi, A. Mebsout, G. Melquiond

- Mohamed.

----
Senior R&D Engineer, OCamlPro
Research Associate, VALS team, LRI.
http://www.iguer.info


Le 16/02/2014 22:01, Dharmalingam Ganesan a ?crit :
> 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
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140217/eb1588ad/attachment.html>