c - 奇妙なクロックワークの検出（バッファオーバーフロー）

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を使用できます。

ここに本当の問題はありますか？存在しない場合、これは非常に明白な誤検知のようです。

Answer 1

このコードには問題はありません。Frama-Cは、このコマンドラインを使用して次のことを確認し frama-c -val -absolute-valid-range 0x10000000-0x10001000 file.c ます。関数本体内にforループを配置した場合。

Klockworkによると、この誤警報はキャストに関連している可能性があります。http：//developer.klocwork.com/community/forums/klocwork-general/general-discussion/buffer-overflow-adjusted-sizeを参照してください。