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: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Sun, 16 Mar 2014 12:12:16 -0400
  • In-reply-to: <5321C6D7.5040407@cea.fr>
  • References: <524082A7.8080202@cea.fr> <20140312182447.GH20864@damazan>,<5321C6D7.5040407@cea.fr>

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)