c - Frama-C 将数组初始化为零规范

Question

我正在尝试证明将两个整数数组初始化为零的 C 循环规范，但我无法验证它。

代码如下:

int first[26];
int second[26];
int c;
/*@
loop assigns first[0..(c-1)];
loop assigns second[0..(c-1)];
loop assigns c; 
loop invariant 0 <= c <= 26;
loop invariant \forall integer k; 0 <= k < c ==> second[k] == first[k];
loop invariant \forall integer k; 0 <= k < c ==> first[k] == 0 && second[k] == 0;
loop invariant \valid(first+(0..25)) && \valid(second+(0..25));
loop variant 26-c;
*/
for(c = 0; c < 26; c++)
{
  first[c] = 0;
  second[c] = 0;
}

我也尝试过使用缩写形式int first[26] = {0}; 用于零初始化，但 Frama-C 似乎不支持该形式。

我将 Frama-C Sodium-20150201 与 Alt-Ergo 证明器一起使用，它无法验证规范的前三个不变量，即

loop invariant 0 <= c <= 26;
loop invariant \forall integer k; 0 <= k < c ==> second[k] == first[k];
loop invariant \forall integer k; 0 <= k < c ==> first[k] == 0 && second[k] == 0;

Answer 1

您的 Frama-C 安装可能有问题，您的代码可以通过默认设置进行完美验证。

我使用的代码:

$ cat loop-init.c 
void loop_init(void)
{
  int first[26];
  int second[26];
  int c;
  /*@
    loop assigns first[0..(c-1)];
    loop assigns second[0..(c-1)];
    loop assigns c; 
    loop invariant 0 <= c <= 26;
    loop invariant \forall integer k; 0 <= k < c ==> second[k] == first[k];
    loop invariant \forall integer k; 0 <= k < c ==> first[k] == 0 && second[k] == 0;
    loop invariant \valid(first+(0..25)) && \valid(second+(0..25));
    loop variant 26-c;
  */
  for(c = 0; c < 26; c++)
    {
      first[c] = 0;
      second[c] = 0;
    }
}

一切都证明了:

$ frama-c -wp loop-init.c 
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing loop-init.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 14 goals scheduled
[wp] [Qed] Goal typed_loop_init_loop_inv_established : Valid
[wp] [Qed] Goal typed_loop_init_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_loop_init_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_loop_init_loop_inv_4_preserved : Valid
[wp] [Alt-Ergo] Goal typed_loop_init_loop_inv_preserved : Valid (16ms) (18)
[wp] [Alt-Ergo] Goal typed_loop_init_loop_inv_2_preserved : Valid (28ms) (26)
[wp] [Qed] Goal typed_loop_init_loop_inv_4_established : Valid
[wp] [Qed] Goal typed_loop_init_loop_assign_part1 : Valid
[wp] [Qed] Goal typed_loop_init_loop_assign_part2 : Valid
[wp] [Qed] Goal typed_loop_init_loop_assign_part3 : Valid
[wp] [Qed] Goal typed_loop_init_loop_assign_part4 : Valid
[wp] [Qed] Goal typed_loop_init_loop_term_decrease : Valid
[wp] [Qed] Goal typed_loop_init_loop_term_positive : Valid
[wp] [Alt-Ergo] Goal typed_loop_init_loop_inv_3_preserved : Valid (1.6s) (68)
[wp] Proved goals:   14 / 14
     Qed:            11 
     Alt-Ergo:        3  (16ms-1.6s) (68)