Frama-C-discuss mailing list archives

dganesan at fc-md.umd.edu (Dharmalingam Ganesan) · Sun, 16 Mar 2014 18:04:49 -0400

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