c - 奇怪的 Klockwork 发现（缓冲区溢出）

Question

我想不通。我有以下代码：

#define SIZE 1000
#define MEMORY 0x10000000

unsigned char table[SIZE];
int i;

for(i=0;i<SIZE;i++) {
    table[i] = *(unsigned char*)(MEMORY +i);
}

Klockwork 告诉我

缓冲区溢出，“表”的数组索引可能超出范围。大小为 1000（调整后大小为 250）的数组“表”可以使用索引值 250..999。

这里真的有问题吗？如果没有，这似乎是一个非常明显的误报。

score 4 · Accepted Answer

此代码没有问题：Frama-C 确认使用此命令行： frama-c -val -absolute-valid-range 0x10000000-0x10001000 file.c 前提是您将 for 循环放在函数体中。

1 回答 1