--- layout: fc_discuss_archives title: Message 36 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,

Added max-split option for this attached program, which worked well with Z3 (all goals proved) but not for Alt-Ergo. Any comments how to make it to work with Alt-Ergo?

Thanks,
Dharma
________________________________________
From: iguernelala mohamed [mohamed.iguernelala at gmail.com] On Behalf Of Mohamed Iguernelala [mohamed.iguernelala at ocamlpro.com]
Sent: Monday, February 17, 2014 12:26 PM
To: Dharmalingam Ganesan; Frama-C public discussion
Subject: Re: [Frama-c-discuss] Frama-c: WP issues with Alt-Ergo (but works with Z3)

 I wonder if you could comment under what circumstances I should use this -max-split option.
Unfortunately, -max-spit is just a heuristic. We are investigating the improvement of our "case split analysis" method described in [1] to get rid of this "frustrating" limitation.

- Mohamed.


From: frama-c-discuss-bounces at lists.gforge.inria.fr<mailto:frama-c-discuss-bounces at lists.gforge.inria.fr> [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Mohamed Iguernelala
Sent: Monday, February 17, 2014 1:42 AM
To: frama-c-discuss at lists.gforge.inria.fr<mailto:frama-c-discuss at lists.gforge.inria.fr>
Subject: Re: [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<http://cp.mcafee.com/d/FZsS921J5AQsFK8CzBBZATsSDtV5VxxZ5cSDtV5VxxZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdzDTthKO_R-hK-qekQT-LsKCPtDAmjhOPtBzBHEShhlKYzOEuvkzaT0QSyrjdTV5xdVYsyMCqejtPo0ah5LUZa3JjrItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdEI6zBdYS2_id41Fr5UWHFuNt2lbdQEqnjh0bNRniZAzh00Emd44Gkr-xEwciCjd40wvcKdh8Rd41EE8dPd41yIiJ3h0oBcCq809pd59IsMryffg>




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<mailto:Frama-c-discuss at lists.gforge.inria.fr>

http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss<http://cp.mcafee.com/d/avndz8w939J5AQsFK8CzBBZATsSDtV5VxxZ5cSDtV5VxxZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdzDTthKO_R-hK-qekQT-LsKCPtDAmjhOPtBzBHEShhlKYzOEuvkzaT0QSCrjdTV5xdVYsyMCqejtPo0c-l9QUyW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafBite8Kw0vWk8OTDoCQm3hOC-r1vF6y0QJyYtlQLoKxaBCWkdbFEw5UWHFuOhEw0kb6y2lad_gQg69j9Cy0gfCn6EAqCy0Qk46VCy0Nm9mxEwciCjd404ICyASeodCp5eP5cM>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_array.c
Type: text/x-csrc
Size: 661 bytes
Desc: max_array.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140218/48951c70/attachment.c>