使用Frama-C验证C代码内存访问合法性的问题求助

这个警告并非Frama-C Eva的不可突破的能力限制，你可以通过优化ACSL注释（尤其是添加循环不变式）或者升级Frama-C版本来完成验证，消除越界读取的告警。

问题回顾 #

你提供的LEB128读取函数及ACSL注释如下：

/*@ requires \valid(ptr);
    requires \valid_read((*ptr) + (0 .. (end-*ptr)));
    assigns *ptr; */
int read_leb128(char **ptr, char *end) {
    int r = 0;
    int s = 0;
    char b;
    do {
        if ((intptr_t)*ptr >= (intptr_t)end) (exit(1));
        b = *(*ptr)++;
        r += (b & (char)0x7f) << s;
        s += 7;
    } while (b & (char)0x80);
    return r;
}

运行Frama-C 19.0（Potassium）的Eva插件后，出现警告：

[eva:alarm] foo.c:33: Warning: out of bounds read. assert \valid_read(tmp); (tmp from *ptr++)

告警原因 #

Frama-C 19.0的Eva插件在处理循环内的指针递增和前置边界检查时，自动关联能力有限。虽然你代码里有if ((intptr_t)*ptr >= (intptr_t)end) exit(1);的运行时检查，但Eva无法自动推断出这个检查能保证后续*(*ptr)++的内存访问是合法的，因此抛出了告警。

解决方法 #

方法1：添加循环不变式明确约束 #

通过ACSL的循环不变式，向Eva明确循环过程中指针的合法范围和内存访问的有效性，帮助工具完成验证。修改后的代码及注释如下：

/*@ requires \valid(ptr);
    requires \valid_read((*ptr) + (0 .. (end-*ptr)));
    assigns *ptr;
    ensures \old(*ptr) <= *ptr <= end;
    // 循环不变式：定义每次迭代开始时的状态约束
    loop invariant \valid(ptr);
    loop invariant \old(*ptr) <= *ptr <= end;
    loop invariant \valid_read(*ptr);
    loop invariant s == 7 * (\at(*ptr, LoopEntry) - *ptr);
    loop assigns *ptr, r, s, b;
    loop variant end - *ptr;
*/
int read_leb128(char **ptr, char *end) {
    int r = 0;
    int s = 0;
    char b;
    do {
        if ((intptr_t)*ptr >= (intptr_t)end) (exit(1));
        b = *(*ptr)++;
        r += (b & (char)0x7f) << s;
        s += 7;
    } while (b & (char)0x80);
    return r;
}

各不变式的作用：

• \old(*ptr) <= *ptr <= end：确保指针始终在初始位置到end的合法区间内
• \valid_read(*ptr)：明确当前指针指向的内存是可读的
• loop variant end - *ptr：告诉Eva循环会终止（指针每次递增，与end的距离不断减小）
• loop assigns：明确循环内修改的变量，帮助Eva跟踪状态变化

方法2：显式添加内存访问断言 #

在读取指针指向的内存前，显式添加断言确认内存可读，虽然有点冗余，但可以直接消除告警：

do {
    if ((intptr_t)*ptr >= (intptr_t)end) (exit(1));
    /*@ assert \valid_read(*ptr); */
    b = *(*ptr)++;
    r += (b & (char)0x7f) << s;
    s += 7;
} while (b & (char)0x80);

方法3：升级Frama-C版本 #

Frama-C 20.0及后续版本对Eva的指针分析和循环推理能力做了改进，能够更好地自动关联你的运行时边界检查和内存访问操作，可能不需要额外添加复杂注释就能通过验证。如果环境允许，升级到新版本是更省心的选择。

总结 #

这个告警是特定版本Eva的分析局限性导致的，并非无法解决。通过上述任意一种方法，都可以完成函数的内存安全性验证，消除越界读取的警告。

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