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] WP Question/Bug?


  • Subject: [Frama-c-discuss] WP Question/Bug?
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Tue, 18 Mar 2014 17:32:07 +0100
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7BF6BF32A@Mail1.FCMD.local>
  • References: <524082A7.8080202@cea.fr> <20140312182447.GH20864@damazan> <5321C6D7.5040407@cea.fr> <B517F47C2F6D914AA8121201F9EBEE6701C7BF7302D1@Mail1.FCMD.local>, <CAEt_dErYv5ac=nOH-UYTF1oU-ta14XVzUFg8g8WoCEVM1_y1Dw@mail.gmail.com> <B517F47C2F6D914AA8121201F9EBEE6701C7BF7302D2@Mail1.FCMD.local> <53277A35.1050608@inria.fr> <B517F47C2F6D914AA8121201F9EBEE6701C7BF6BF32A@Mail1.FCMD.local>

Simply remove the \forall.
Then, you will have to prove that j(j+1)/2 + (j+1) == (j+1)(j+2)/2.
Finally, this may require the field tactic of Coq or an SMT solver with strong non-linear arithmetics (which is uncommon).
	L.

Le 17 mars 2014 ? 23:48, Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit :

> Hi,
> 
> Thanks. I have not done a lot of annotations. I thought for all j  < i, we have computed sum of 1+2+3...+j, which is j(j+1)/2.
> 
> If this is wrong, how will you repair it? Is there a notion of built-in sum which WP understands?
> 
> Thanks once again.
> Dharma
> 
> -----Original Message-----
> From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Claude Marche
> Sent: Monday, March 17, 2014 6:42 PM
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: Re: [Frama-c-discuss] WP Question/Bug?
> 
> 
> SMT solvers like Alt-Ergo, CVC and Z3 can partly deal with non-linear integer formulas, like the one of your example. No need for interactive provers there.
> 
> The main issue is that your annotations are wrong, e.g. a formula like
> 
>   for integer j between 0 and i, sum == j*(j+1)/2
> 
> cannot be valid, obviously.
> 
> Debugging annotations is not a simple task. Maybe you could give a try at E-ACSL, which might help you to find simple errors using simple tests.
> 
> Indeed using an interactive prover like Coq is also a good way to discover false or missing annotations. But learning Coq is not a trivial thing...
> 
> Hope this helps,
> 
> - Claude
> 
> 
> On 03/16/2014 11:04 PM, Dharmalingam Ganesan wrote:
>> Hi,
>> 
>> I'm using WP to prove the following C program, which is intended to sum the first n natural numbers.  
>> 
>> I'm not sure how one will prove such non-linear constraints. I'm not an expert in Coq. Can any one point me to an example of how an interactive-prover can be used to prove this  C program is correct?
>> 
>> 
>> /*@
>>  @ ensures \result == n*(n+1)/2;
>>  @*/
>> int sum_1_n(unsigned int n) {
>>  int sum = 0;
>>  int i = 0;
>> 
>>  /*@ 
>>      loop invariant 0<=i<=n+1;
>> 
>>      loop invariant \forall integer j;
>>         0 < j < i ==> sum == j*(j+1)/2;
>> 
>>      loop assigns i, sum;
>> 
>>      loop variant n-i;
>>  */
>>  for(i=0; i <= n; i++)
>>  {
>>    sum +=i;
>>  }
>> 
>>  return sum;
>> }
>> 
>> 
>> 
>> 
>> 
>> 
>> [formal_verification]$ frama-c -wp sum_1_n.c [kernel] preprocessing 
>> with "gcc -C -E -I.  sum_1_n.c"
>> [wp] Running WP plugin...
>> [wp] Collecting axiomatic usage
>> [wp] warning: Missing RTE guards
>> [wp] 8 goals scheduled
>> [wp] [Alt-Ergo] Goal typed_sum_1_n_loop_inv_established : Valid (16ms) 
>> (6) [wp] [Alt-Ergo] Goal typed_sum_1_n_loop_inv_preserved : Valid 
>> (16ms) (13) [wp] [Qed] Goal typed_sum_1_n_loop_assign : Valid [wp] 
>> [Qed] Goal typed_sum_1_n_loop_term_decrease : Valid [wp] [Alt-Ergo] 
>> Goal typed_sum_1_n_loop_inv_2_established : Valid (8ms) (3) [wp] 
>> [Alt-Ergo] Goal typed_sum_1_n_loop_term_positive : Valid (8ms) (12) 
>> [wp] [Alt-Ergo] Goal typed_sum_1_n_post : Unknown (6s) [wp] [Alt-Ergo] 
>> Goal typed_sum_1_n_loop_inv_2_preserved : Timeout (Qed:4ms)
>> [wp] Proved goals:    6 / 8
>>     Qed:             2 
>>     Alt-Ergo:        4  (8ms-16ms) (13) (interruped: 1) (unknown: 1)
>> 
>> 
>> ________________________________________
>> From: frama-c-discuss-bounces at lists.gforge.inria.fr 
>> [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Cristiano 
>> Sousa [cristiano.sousa126 at gmail.com]
>> Sent: Sunday, March 16, 2014 1:07 PM
>> To: Frama-C public discussion
>> Subject: Re: [Frama-c-discuss] WP Question/Bug?
>> 
>> Hi,
>> 
>> You seem to be missing your loop variant and an invariant indicating how the 'i' variable is bound. You should add:
>> 
>>      loop invariant -1 <= i < n;
>>      loop variant i;
>> 
>> With this, the generated memory safety annotations are discharged. However, your post-conditions are not.
>> 
>> In situations like this I prefer to annotate each possible outcome of the function using different behaviors. In your case it would look like this:
>> 
>> 
>> /*@
>>  requires n>=0 && \valid(t+(0..n-1));
>>  assigns \nothing;
>> 
>>  behavior zero_size:
>>    assumes n == 0;
>>    ensures \result == 0;
>>  behavior no_zero:
>>    assumes n > 0;
>>    assumes \forall integer j; 0 <= j < n ==> t[j] != 0;
>>    ensures \result == 0;
>>  behavior has_zero:
>>    assumes n > 0;
>>    assumes \exists integer j; 0 <= j < n && t[j] == 0;
>>    ensures t[\result] == 0;
>>    ensures 0 <= \result < n;
>>    ensures \forall integer j; j > \result && j < n ==> t[j] != 0;
>> 
>>  complete behaviors;
>>  disjoint behaviors;
>> */
>> int get_max_index(int t[], int n)
>> {
>>  int i = 0;
>> 
>>  /*@
>>      loop invariant -1 <= i < n;
>>      loop invariant \forall integer j; j > i && j < n ==>  \at(t[j], Pre) != 0;
>>      loop assigns i;
>>      loop variant i;
>>   */
>> 
>>  for(i = n-1; i >=0 ; i--)
>>  {
>>    if(t[i] == 0) return i;
>>  }
>> 
>>  return 0;
>> }
>> 
>> 
>> The annotation are longer, but I find it much easier to understand. 
>> The above annotations are fully discharged using Frama-C Fluorine 2 
>> and alt-ergo 0.95.1
>> 
>> 
>> 
>> 2014-03-16 16:12 GMT+00:00 Dharmalingam Ganesan <dganesan at fc-md.umd.edu<mailto:dganesan at fc-md.umd.edu>>:
>> Hi,
>> 
>> I do not understand why the first ensures as well as the generated valid memory access within the loop are not provable. I tried it on the latest version of Frama-c.
>> 
>> 
>> /*@ logic integer max_index{L}(int* t, integer n) =
>>  @   (n==0) ? 0 :
>>  @   (t[n-1] == 0) ? n-1 : max_index(t, n-1);
>> */
>> 
>> /*@
>>   requires n>=0 && \valid(t+(0..n-1));
>>   assigns \nothing;
>>   ensures \result == max_index(t, n);
>>   ensures \forall integer j; j > \result && j < n ==> t[j] != 0; */ 
>> int get_max_index(int t[], int n) {
>>  int i = 0;
>> 
>>  /*@ loop invariant \forall integer j;
>>        j > i && j < n ==>  \at(t[j], Pre) != 0;
>> 
>>      loop assigns i;
>>   */
>> 
>>  for(i = n-1; i >=0 ; i--)
>>  {
>>    if(t[i] == 0) return i;
>>  }
>> 
>>  return 0;
>> }
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>> [formal_verification]$ frama-c -wp -wp-rte max_index.c [kernel] 
>> preprocessing with "gcc -C -E -I.  max_index.c"
>> [wp] Running WP plugin...
>> [wp] Collecting axiomatic usage
>> [rte] annotating function get_max_index [rte] annotating function main 
>> [wp] 14 goals scheduled [wp] [Alt-Ergo] Goal 
>> typed_get_max_index_assert_rte_signed_overflow : Valid (8ms) (9) [wp] 
>> [Alt-Ergo] Goal typed_get_max_index_loop_inv_preserved : Valid (20ms) 
>> (26) [wp] [Alt-Ergo] Goal typed_get_max_index_post_2 : Valid (24ms) 
>> (27) [wp] [Qed] Goal typed_get_max_index_loop_inv_established : Valid 
>> [wp] [Qed] Goal typed_get_max_index_loop_assign : Valid [wp] [Qed] 
>> Goal typed_get_max_index_assign_part1 : Valid (4ms) [wp] [Qed] Goal 
>> typed_get_max_index_assign_part2 : Valid [wp] [Alt-Ergo] Goal 
>> typed_get_max_index_assert_rte_signed_overflow_2 : Valid (20ms) (16) 
>> [wp] [Qed] Goal typed_get_max_index_assign_part3 : Valid [wp] 
>> [Alt-Ergo] Goal typed_get_max_index_assert_rte_mem_access : Unknown 
>> (1s) [wp] [Qed] Goal typed_get_max_index_assign_part4 : Valid [wp] 
>> [Qed] Goal typed_get_max_index_assign_part5 : Valid [wp] [Qed] Goal 
>> typed_main_call_get_max_index_pre : Valid [wp] [Alt-Ergo] Goal 
>> typed_get_max_index_post : Unknown (Qed:4ms) (6s)
>> [wp] Proved goals:   12 / 14
>>     Qed:             8  (4ms-4ms)
>>     Alt-Ergo:        4  (8ms-24ms) (27) (unknown: 2)
>> 
>> 
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gfo
>> rge.inria.fr> 
>> http://cp.mcafee.com/d/avndy1J5AQsLTd7bybdPtPqtTAnC67QkPqtTAnC67T6jqtT
>> AnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISWPEUsCO_R-juvd78
>> W_nKnjjvoVxNxVN_BHFShhlKYPOEuvkzaT0QSyrodTV5xdVYsyMCqejtPo0c-l9QUyW01_
>> Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafBite8K
>> w0vWk8OTDoCQrLL8CMnWhEwdboL7ltbSbEiFpKB3iWq8052NEw0tLWjBm63bp4ArpudJns
>> h<http://cp.mcafee.com/d/k-Kr4x8idEICzBwQsL6zBNVUTsSDtV5VxxZ5cSDtV5Vxx
>> ZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdK3JgvjpvW_
>> cK9KcTjWZOW8WX7fFCzBWXP7bnhIyyHtBDBgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYG
>> jFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0
>> kvaAWsht00_QEhBLeNdEI3HzzobZ8Qg6BInzGKBX5Q9kITixFtd402xoQg0eTZ9OH31BIy
>> idIL6_f9Zc-TD>
>> 
>> 
>> 
>> --
>> Cumprimentos,
>> Cristiano Sousa
>> 
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr
>> http://cp.mcafee.com/d/FZsS73gw821J5AQsLTd7bybdPtPqtTAnC67QkPqtTAnC67T
>> 6jqtTAnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISWPEUsCO_R-j
>> uvd78W_nKnjjvoVxNxVN_BHFShhlKYPOEuvkzaT0QSCrodTV5xdVYsyMCqejtPo0c-l9QU
>> yW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafB
>> ite8Kw0vWk8OTDoCQrLL8CMnWhEwdboL7ltbSbEiFpKB3iWq8052NEw0tLWjBm63bp4Arp
>> udKR8_qNQpU4II
>> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://cp.mcafee.com/d/FZsS820O83hJ5AQsLTd7bybdPtPqtTAnC67QkPqtTAnC67T6jqtTAnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISWPEUsCO_R-juvd78W_nKnjjvoVxNxVN_BHFShhlKYPOEuvkzaT0QSOrodTV5xdVYsyMCqejtPo0c-l9QUyW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafBite8Kw0vWk8OTDoCQrLL8CMnWhEwdboL7ltbSbEiFpKB3iWq8052NEw0tLWjBm63bp4ArpudBNzpC-Z0iC4O
> 
> _______________________________________________
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140318/cfe679eb/attachment-0001.html>