Odd Klockwork finding (Buffer overflow)

Question

I can't figure this out. I have the following code:

#define SIZE 1000
#define MEMORY 0x10000000

unsigned char table[SIZE];
int i;

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

And Klockwork tells me

Buffer overflow, array index of 'table' may be out of bounds. Array 'table' of size 1000 (adjusted size 250) may use index value(s) 250..999.

Is there a real problem here? This seems an awfully obvious false positive if there isn't.

Answer 1

This code has no problems: Frama-C confirms that using this command line: frama-c -val -absolute-valid-range 0x10000000-0x10001000 file.c provided you put the for loop inside a function body.

According to Klockwork, this false alarm could be related to your cast: see http://developer.klocwork.com/community/forums/klocwork-general/general-discussion/buffer-overflow-adjusted-size