frama-c - 无法证明分配子句 - Frama-C

Question

我是 Frama-c 的新手，我想了解这个简单示例有什么问题：

/*@ requires \valid(array+(0..length-1))
@ ensures \forall integer k; 0 <= k < length ==> array[k] == 0;
@ assigns array[0..length-1];
*/
void fill(int array[], int length){
    /*@ loop invariant 0 <= i <= length;
    @ loop invariant \forall integer k; 0 <= k < i ==> array[k] == 0;
    @ loop assigns i, array[0..i-1];
    @ loop variant length - i;
    */
    for(int i = 0; i < length; i++){
        array[i] = 0;
    }
}

在此示例中，Frama-c (WP + Value) 不会证明函数合同中的分配子句，我不明白为什么。任何帮助将不胜感激 =)

Answer 1

如果您削弱循环分配，则可以证明这一点（使用 alt-ergo 0.95.1）。

@loop 赋值 i, array[0..length-1];

前提条件i >= 0也是需要的，因为它没有被暗示\valid(array+(0..length-1)。array+(0..length-1)是一组有效的位置length <= 0，虽然是一个空位置。

您的原始循环分配的事实并不意味着您的先决条件是 WP 插件当前版本的限制。