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

【问题标题】：Frama-C initialize array to zero specificationFrama-C 将数组初始化为零规范
【发布时间】：2015-08-19 20:05:14
【问题描述】：

我正在尝试证明将两个整数数组初始化为零的 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;

【问题讨论】：

你从 0 循环到 26 排他，所以0 <= c < 26 (0 <= c <= 25)。
不支持memset之类的东西吗？在这种情况下，您可以简单地使用memset(first, 0, 26 * sizeof(int))。
@Kninnug 请参阅下面的第二条评论stackoverflow.com/questions/32144221/…

标签： c frama-c

【解决方案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)

【讨论】：

谢谢，已解决！是安装Alt-Ergo的问题（好像没有安装），所以我从'apt-get'获取，然后运行成功！