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: Tue, 18 Feb 2014 23:43:54 -0500
  • In-reply-to: <5302464C.5000906@ocamlpro.com>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C76682DC29@Mail1.FCMD.local>, <52D6B7B0.4020005@fr.merce.mee.com> <B517F47C2F6D914AA8121201F9EBEE6701C7BB59DEAB@Mail1.FCMD.local> <5301AF4D.6050500@ocamlpro.com> <B517F47C2F6D914AA8121201F9EBEE6701C7BB53DF2D@Mail1.FCMD.local>, <5302464C.5000906@ocamlpro.com>
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>