Frama-C-discuss mailing list archives

mohamed.iguernelala at ocamlpro.com (Mohamed Iguernelala) · Mon, 17 Feb 2014 18:26:36 +0100

> 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] *On Behalf Of 
> *Mohamed Iguernelala
> *Sent:* Monday, February 17, 2014 1:42 AM
> *To:* 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 --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140217/aec93f00/attachment-0001.html>

Frama-C-discuss mailing list archives

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