奇怪的 Klockwork 发现（缓冲区溢出）答案

【问题标题】：Odd Klockwork finding (Buffer overflow)奇怪的 Klockwork 发现（缓冲区溢出）
【发布时间】：2011-08-24 05:52:14
【问题描述】：

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

#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。

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

【问题讨论】：

【解决方案1】：

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

【讨论】：

谢谢，解决了。我会将这些标记为“不是问题”。
同意；特别是，请参阅 Kirill Zhegulev 于 2011 年 4 月 28 日关于缺少包含文件或宏定义的评论。正确处理这些问题至关重要，否则您最终可能会浪费大部分时间。根据我的经验，如果“调整后的大小”小于原始大小（尤其是为零时），则报告几乎总是误报。但如果调整后的尺寸比原来的尺寸大，那很可能是正确的。