为何Frama-C中最后一个断言无法验证？

我正在使用Frama-C 29.0（Copper），编写了如下带有形式化规范的C函数：

typedef struct __CheckCal {
    int len;
    int *pkv;
    int chksum;
} CheckCal;

/*@
axiomatic SumArray {
    logic integer sum(int* array, integer begin, integer end) 
        reads array[begin .. end-1];

    axiom empty:
        \forall int* a, integer b, e; b >= e ==> sum(a, b, e) == 0;

    axiom range:
        \forall int* a, integer b, e; b < e ==> 
            sum(a, b, e) == sum(a, b, e-1) + a[e-1];
}
*/

/*@
    requires \valid(pIp);
    requires \valid(pIp->pkv + (0..pIp->len-1));
    requires 0 <= pIp->len <= 10;
*/
void CheckCal(CheckCal *pIp)
{
    int i = 0;
    int chksum = 0;

    /*@
        loop invariant (0 < \at(pIp,Pre)->len) ==> 
                       (0 <= i <= \at(pIp,Pre)->len);
        loop invariant (0 < \at(pIp,Pre)->len) ==> 
                       (chksum == sum(pIp->pkv, 0, i));
        loop invariant pIp == \at(pIp,Pre);
        loop invariant pIp->len == \at(pIp->len,Pre);
        loop invariant \forall integer j; 
            0 <= j < pIp->len ==> pIp->pkv[j] == \at(pIp->pkv[j],Pre);
    */
    for (; i < pIp->len; i++) {
        chksum = chksum + pIp->pkv[i];
    }

    /*@ assert (0 < \at(pIp,Pre)->len) ==> 
                 (chksum == sum(pIp->pkv, 0, pIp->len)); */   // 可验证通过

    pIp->chksum = chksum;

    /*@ assert (0 < \at(pIp,Pre)->len) ==> 
                 (pIp->chksum == sum(pIp->pkv, 0, pIp->len)); */  // 验证失败
}

在此设置下，涉及局部变量chksum的倒数第二个断言可成功验证，但涉及结构体字段pIp->chksum的最后一个断言无法被证明。请问Frama-C为何接受前者却拒绝后者？这是否与结构体字段的不变量处理方式，或是循环后赋值语句pIp->chksum = chksum的传播机制有关？

问题原因分析 #

核心问题出在**sum逻辑函数的reads子句**以及Frama-C对内存写入操作的默认处理逻辑上：

1. sum函数的读取依赖约束
   你的sum逻辑函数声明了reads array[begin .. end-1];，这意味着Frama-C会认为sum的取值严格依赖指定范围内的数组内存内容。当执行pIp->chksum = chksum;赋值操作时，Frama-C的默认分析会认为：写入结构体字段可能间接修改pIp->pkv的地址（尽管你的代码实际没有修改，但验证器不会主动排除这种潜在可能性），进而导致之前关于sum(pIp->pkv, ...)的结论失效。

2. 断言上下文的中断
   倒数第二个断言验证通过时，验证器的上下文明确记录了chksum与sum(pIp->pkv, 0, pIp->len)的等价关系。但赋值操作触发了内存状态的变更标记，验证器会丢弃与pIp指向内存相关的旧结论，无法直接将chksum的等价关系传递到结构体字段的断言中。

3. 循环不变量的覆盖不足
   现有循环不变量仅保证了数组元素的稳定性，但未明确pIp->pkv本身的地址未被修改。验证器无法自动将“数组元素不变”推导为“数组指针未变、sum的依赖未被破坏”。

修复方案 #

可以通过以下方式快速解决验证失败问题：

增强循环不变量，明确数组指针的稳定性 #

在循环不变量中添加一条，明确pIp->pkv的地址始终等于初始值：

loop invariant pIp->pkv == \at(pIp->pkv, Pre);

这条不变量会告知验证器：pIp->pkv从未被修改，数组的内存依赖关系在赋值操作后依然成立，最后一个断言就能顺利验证通过。

内容的提问来源于stack exchange，提问作者user18397851