Frama-C 正在证明无效断言

Question

我能够使用 Frama-C 证明以下程序，这令人惊讶，因为 1) 存在断言 false，以及 2) 循环不变量不成立（数组 a 包含 1 而不是 2 ).我在这里遗漏了什么吗？

/*@ requires \valid(a+ (0..9)) && \valid(b+ (0..9));
 */
void test_foo(int *a, char *b) {
  int i = 0;
  /*@ loop invariant \forall int j; 0 <= j < i ==> a[j] == 2; 
      loop invariant \forall int j; 0 <= j < i ==> b[j] == 'a';
   */
  for (int i = 0; i < 10; i++) {
    a[i] = 1;
    b[i] = 'a';
  }   
  //@ assert \false;
}

我是运行 frama-c 作为： frama-c -wp -wp-invariants -wp-prover "why3:alt-ergo" -wp-model "Typed,int,real" -wp-par 8 -wp-timeout 15 -wp-out wp.out test.c 我在 Sodium 和 Magnesium 版本上看到相同的行为。

Answer 1

-wp-invariants 并不意味着处理 "normal" 循环不变量，例如您提供的那些，而是 "general inductive invariants" 在 ACSL section 2.4.2 的意义上。因此，您可以从命令行中删除此选项。然后一些证明义务如预期的那样失败了。

另外请注意，您的循环注释不完整：正如 WP 警告的那样，您应该有一个循环分配，例如

loop assigns i, a[0 .. 9], b[0 .. 9];

然后，为了能够证明这个loop assigns，你需要指定i变化区间：

loop invariant 0<=i<=10;

最后，-wp-invariants 使证明义务在存在正常循环注释的情况下表现异常这一事实可能应该被视为一个错误并在 Frama-C's bts 上报告。

Frama-C 正在证明无效断言

Frama-C is proving invalid assertions

frama-c