Frama-C wp 简单循环不变量

Question

我在尝试使用 wp 插件证明以下程序时遇到一个非常简单的循环不变式的问题：

void f() {
  unsigned int i = 0;
  /*@
   loop assigns i;
   loop invariant 0 <= i <= 2;
   loop variant 2 - i;
  */
  for (;i < 2;++i);
}

输出为：

[kernel] preprocessing with "gcc -C -E -I.  t.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_f_loop_inv_established : Valid
[wp] [Qed] Goal typed_f_loop_assign : Valid
[wp] [Qed] Goal typed_f_loop_term_decrease : Valid (4ms)
[wp] [Qed] Goal typed_f_loop_term_positive : Valid
[wp] [Alt-Ergo] Goal typed_f_loop_inv_preserved : Failed
     Error: Alt-Ergo exits with status [127]

当使用 -wp-print 键执行 frama-c 时，它会打印以下与失败目标相关的信息：

Goal Preservation of Invariant (file t.c, line 5):
Assume {
  (* Domain *)
  Type: (is_uint32 i_1) /\ (is_uint32 (1+i_1)).
  (* Invariant (file t.c, line 5) *)
  (* t.c:8: Invariant: *)
  Have: (0<=i_1) /\ (i_1<=2).
  (* t.c:8: Then *)
  Have: i_1<=1.
}
Prove: -1<=i_1.
Prover Alt-Ergo returns Failed
Error: Alt-Ergo exits with status [127]

Answer 1

在您的配置中，Alt-Ergo 可能配置错误或缺失（return 代码 127）。

您的代码在我的机器上运行没有任何问题：

[wp] [Qed] Goal typed_f_loop_inv_established : Valid
[wp] [Qed] Goal typed_f_loop_assign : Valid
[wp] [Qed] Goal typed_f_loop_term_decrease : Valid
[wp] [Qed] Goal typed_f_loop_term_positive : Valid
[wp] [Alt-Ergo] Goal typed_f_loop_inv_preserved : Valid (40ms) (7)
[wp] Proved goals:    5 / 5
     Qed:             4 
     Alt-Ergo:        1  (40ms-40ms) (7)

是什么给了 alt-ergo -version？

此致，大卫

Frama-C wp 简单循环不变量

Frama-C wp simple loop invariant

frama-c