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

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)