Frama-C处理无限循环吗？

Question

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

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没有处理无限循环？

Answer 1

你的问题有两个层次的答案。

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

• 使用演绎验证，因为在这个简单的示例中，您甚至不需要额外的注释。您可以使用基于Apron的Frama-C/Eva的(实验)关系域来验证frama-c -wp证明了
• 的断言。由于技术原因，这些方法还不适用于断言，因此您应该按以下方式重写代码：

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的结果是

值/home/yakobowski/incr.c:10: Frama_C_show_each：{1} value /home/yakobowski/incr.c:5:开始合并循环迭代value /home/yakobowski/incr.c:10: Frama_C_show_each：{1} value /home/yakobowski/incr.c:10: Frama_C_show_each：{1}值:alarm /home/yakobowski/incr.c:7:警告:签名溢出。assert count +1 Frama_C_show_each 2147483647；≤/home/yakobowski/incr.c:10: incr.c：{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为真的假设下成立的，这在您的代码中是不可证明的。