--- layout: fc_discuss_archives title: Message 32 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)



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>