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: Jean-Christophe.Filliatre at lri.fr (Jean-Christophe Filliatre)
  • Date: Wed, 19 Feb 2014 11:19:09 +0100
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7BB53E00B@Mail1.FCMD.local>
  • 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> <B517F47C2F6D914AA8121201F9EBEE6701C7BB53E00B@Mail1.FCMD.local>

Hi,

I know this is not your question, but it seems to me that there are a
few mistakes in your code:

- first, "\exists i. A ==> B" shoud rather be "\exists i. A && B" (in
the post and in the loop invariant)

- second, a loop invariant "i <= n" is missing, so that we can prove i =
n when exiting the loop.

With these 3 fixes, everything is proved by Alt-Ergo (and other SMT as
well).


/*@ requires n > 0 && \valid(t+(0..n-1));
  @ requires n < UINT_MAX;
  @ requires \forall integer i; 0<=i<n ==> t[i] >= 0;
  @ ensures \forall integer i; 0<=i<n ==> t[i] <= \result;
  @ ensures \exists integer i; 0<=i<n && t[i] == \result;
  @ assigns \nothing;
  @*/
int max_array(int t[], unsigned int n) {
  int m;
  unsigned int i = 0;
  m = t[0];

  /*@ loop invariant \forall integer j;
        0 <= j < i ==> m >= \at(t[j], Pre);

      loop invariant \exists integer j;
         0 <= j < i && m == \at(t[j], Pre);

      loop invariant i <= n;

      loop assigns m,i;
  */
  for(i=1; i < n; i++)
  {
    if (t[i] > m) {  m = t[i]; }
  }

  return m;
}

Hope this helps,
--
Jean-Christophe



On 19/02/2014 05:43, Dharmalingam Ganesan wrote:
> 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>
> 
> 
> 
> 
> _______________________________________________
> 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
>