--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on March 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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>:

> 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
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Cumprimentos,
Cristiano Sousa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140316/82722250/attachment.html>