是否在 Frama-C 中处理无限循环？答案

【问题标题】：Are infinite loops handled in Frama-C?是否在 Frama-C 中处理无限循环？
【发布时间】：2018-06-26 00:24:31
【问题描述】：

我试图证明变量的值总是增加的。我写了以下代码：

void Commit() {
    int count = 1;
    //@ ghost int old_count = 0;

    while (1) {
        //@ ghost old_count = count;
        count++;
        //@ assert count > old_count;
    }
}

int main () {
    Commit();
    return 0;
}

然后我使用命令：frama-c -val file.c，但断言状态仍然未知。我在这里错过了一些非常基本的东西吗？还是 Frama-C 没有处理无限循环？

【问题讨论】：

标签： frama-c

【解决方案1】：

您的问题有两个级别的答案。

1) 您想证明old_count 和count 之间的关系属性。默认情况下，这种分析在 Frama-C/Eva 中不可用，并且您的断言没有得到证实。您可以：

使用演绎验证，因为在这个简单的示例中，您甚至不需要额外的注释。你可以验证frama-c -wp 证明了这个断言

使用基于 Apron 的 Frama-C/Eva 的（实验性）关系域。由于技术原因，这些还不能用于断言，所以你应该用以下方式重写你的代码：

void Commit() {
    int count = 1;
    //@ ghost int old_count = 0;

    while (1) {
        //@ ghost old_count = count;
        count++;
        /*@ ghost
          int d = count - old_count;
          Frama_C_show_each(d);
        */
    }
}

frama-c -val -eva-apron-oct的结果是

[value] /home/yakobowski/incr.c:10: Frama_C_show_each: {1}
[value] /home/yakobowski/incr.c:5: starting to merge loop iterations
[value] /home/yakobowski/incr.c:10: Frama_C_show_each: {1}
[value] /home/yakobowski/incr.c:10: Frama_C_show_each: {1}
[value:alarm] /home/yakobowski/incr.c:7: Warning: 
  signed overflow. assert count + 1 ≤ 2147483647;
[value] /home/yakobowski/incr.c:10: Frama_C_show_each: {1}

d 的值始终为 1，这是预期值。没有选项-eva-apron-oct，你会得到

[value] /home/yakobowski/incr.c:10: Frama_C_show_each: [-2147483645..2147483646]

在最后一次迭代中。

2) 从验证的角度来看，您的示例没有意义，因为 C 中不存在诸如不断增加的变量之类的东西。您的代码只有在 count < 2147483647 时才是正确的。相反，当它们相等时，您的代码会在count++ 行上导致未定义的行为。这就是 Eva 在这条线上发出警报的原因。

请注意，这一事实不会使我在 1) 中所做的分析无效。 WP 或 Eva 所做的所有推理都是在 count + 1 ≤ 2147483647 为真的假设下成立的，这在您的代码中无法证明。

【讨论】：

关于第 2 点：在看到来自 Frama-C 的警告（并意识到溢出的可能性）后，我在循环条件中包含了对计数的检查，但我没有将其包含在问题中，因为我认为可能有一个解决方法而不排除它。无论如何，感谢您的回答，它非常有用。