Нечетное нахождение часовых механизмов - PullRequest
4 голосов
/ 24 августа 2011

Я не могу понять это. У меня есть следующий код:

#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 говорит мне

Переполнение буфера, индекс массива 'table' может выходить за пределы. Массив 'table' размера 1000 (скорректированный размер 250) может использовать значение (я) индекса 250..999.

Есть ли здесь реальная проблема? Это кажется совершенно очевидным ложным положительным результатом, если его нет.

1 Ответ

4 голосов
/ 24 августа 2011

Этот код не имеет проблем: 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

...