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

Thanks for pointing the issues in my annotation.

I tried your suggestion. Now Alt-Ergo works fine but not  Z3, which is unable to prove a loop invariant. 



[formal_verification]$ frama-c -wp -wp-rte -wp-proof=z3 -pp-annot max_array.c -wp-why-opt=-t,500  -wp-timeout=5000
[kernel] preprocessing with "gcc -C -E -I.  -dD max_array.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function max_array
[wp] 17 goals scheduled
[wp] [Qed] Goal typed_max_array_loop_inv_preserved : Valid
[wp] [Qed] Goal typed_max_array_loop_inv_established : Valid (4ms)
[wp] [Z3] Goal typed_max_array_assert_rte_mem_access : Valid (10ms)
[wp] [Z3] Goal typed_max_array_post : Valid (Qed:4ms) (10ms)
[wp] [Qed] Goal typed_max_array_loop_inv_3_preserved : Valid
[wp] [Qed] Goal typed_max_array_loop_inv_3_established : Valid
[wp] [Z3] Goal typed_max_array_assert_rte_mem_access_2 : Valid (20ms)
[wp] [Qed] Goal typed_max_array_assert_rte_mem_access_3 : Valid (4ms)
[wp] [Z3] Goal typed_max_array_loop_inv_2_established : Valid (130ms)
[wp] [Qed] Goal typed_max_array_loop_assign : Valid
[wp] [Qed] Goal typed_max_array_assign_part1 : Valid
[wp] [Qed] Goal typed_max_array_assign_part2 : Valid
[wp] [Qed] Goal typed_max_array_assign_part3 : Valid
[wp] [Qed] Goal typed_max_array_assign_part4 : Valid
[wp] [Z3] Goal typed_max_array_assert_rte_unsigned_overflow : Valid (10ms)
[wp] [Z3] Goal typed_max_array_post_2 : Valid (11.9s)
[wp] [Z3] Goal typed_max_array_loop_inv_2_preserved : Unknown (8'47s)


________________________________________
From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Jean-Christophe Filliatre [Jean-Christophe.Filliatre at lri.fr]
Sent: Wednesday, February 19, 2014 5:19 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)

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://cp.mcafee.com/d/5fHCMUe6hESyOqekTHLTd7apKVJeXObP33WapJeXObP33Xz9JeXObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSrjZxVyXb_nVYsYUOZvHTbEzxP73zhOqejhOqekrYJt6OaaGdSel3PWApmU6CQjrxK_8I9LfzAm4PhOrKr01i8J_7FgtGrtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9J5BCVEVdwLQzh0qmNueGWnIngBiPta6BQQg2YtlQLp8Qg0a5zh1aB6_Eq834FAPh087Pbzkidjh0qa23sPh0oH4HgQg69j9Cy02mjhir7c6PM6m<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://cp.mcafee.com/d/2DRPoscCQmjhOCZt-VEVjdTdFTuhuoovhjdFTuhuoovspdFTuhuoovhodFTujsKMCYCrg8X3Wr05eSbGEsSGxTEdCTr5RkerlgXQ6PqvIfcnpvW_fzDD6nHZuVt4seoUsqejhOqejhOzvBHEShhlhKNOEuvkzaT0QSCrsdTV5xdVYsyMCqejtPo0c-l9QUyW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafBite8Kw0vWk8OTDoCQmmrCzAS2_id41Fr5UWHFuNt2lbdQEqnjh0bNRniZAzh00Emd44Gkr-xEwciCjd40wvcKdh8Rd41EE8dPd41yIiJ3h0oBcCq809pd59IsMrt9vLKE85<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://cp.mcafee.com/d/k-Kr418g43qb9EVjuK_sQsFCXCQXL8LccfEFCQXL8LccfKcCQXL8LccfEI6QXL9KnojujdE4txZdw2Dr5RkerlgXQ6PrJyWG7dGEtW3pJfS7CbILZvDNPPzbR-LsKye7csed79EVd79EVhLORQr8EGEToVkffGhBrwqrpdK6XYyMCY-ehojd79KVI06vaAWsht00_QEhBLeNM12V2kc4RtxxYGjB1SKeNRniZyW4GmrFgSX7ltbSbEiFpKB2V2Hsbvg57OFeD4ng0fZa4prPIjqbbdPhOr1vF6y0QJyYtlQLoKxaBCWkdbFEw5UWHFuOhEw0kb6y2lad_gQg69j9Cy0gfCn6EAqCy0Qk46VCy0Nm9mxEwciCjd404ICyASeodYdg7
>

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/2DRPowd6QmjhOCZt-VEVjdTdFTuhuoovhjdFTuhuoovspdFTuhuoovhodFTujsKMCYCrg8X3Wr05eSbGEsSGxTEdCTr5RkerlgXQ6PqvIfcnpvW_fzDD6nHZuVt4seoUsqejhOqejhOzvBHEShhlhKNOEuvkzaT0QSMrsdTV5xdVYsyMCqejtPo0c-l9QUyW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafBite8Kw0vWk8OTDoCQmmrCzAS2_id41Fr5UWHFuNt2lbdQEqnjh0bNRniZAzh00Emd44Gkr-xEwciCjd40wvcKdh8Rd41EE8dPd41yIiJ3h0oBcCq809pd59IsMrSymfZRmz