Frama-C-discuss mailing list archives

Claude.Marche at inria.fr (Claude Marche) · Mon, 17 Mar 2014 23:41:57 +0100

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.gforge.inria.fr>
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss<http://cp.mcafee.com/d/k-Kr4x8idEICzBwQsL6zBNVUTsSDtV5VxxZ5cSDtV5VxxZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdK3JgvjpvW_cK9KcTjWZOW8WX7fFCzBWXP7bnhIyyHtBDBgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYGjFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdEI3HzzobZ8Qg6BInzGKBX5Q9kITixFtd402xoQg0eTZ9OH31BIyidIL6_f9Zc-TD>
> 
> 
> 
> --
> Cumprimentos,
> Cristiano Sousa
> 
> _______________________________________________
> 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
> 