Указатель, следующий из арифметики на операнде указателя, должен обратиться к элементу того же массива как тот операнд указателя
Указатель, следующий из арифметики на операнде указателя, должен обратиться к элементу того же массива как тот операнд указателя.
Используя неверный массив индекс может привести к ошибочному поведению программы. Выведенные индексы времени выполнения массивов особенно неприятны, потому что они не могут легко проверяться ручным анализом или статическим анализом.
Стандарт C задает создание указателя на один вне конца массива. Правило разрешает Стандарт C. Разыменование указателя на один вне конца массива вызывает неопределенное поведение и несовместимо.
Polyspace® отмечает это правило во время анализа как:
Bug Finder — Array access
out-of-bounds
и Pointer access
out-of-bounds
.
Программа автоматического доказательства кода — Illegally dereferenced pointer
(Polyspace Code Prover) и Out
of bounds array index
(Polyspace Code Prover).
Bug Finder и Программа автоматического доказательства Кода проверяют это правило по-другому и могут показать различные результаты для этого правила. В Программе автоматического доказательства Кода можно также видеть различие в результатах на основе выбора для опции. Смотрите Проверку на Кодирование Стандартных Нарушений.
Если вы ожидаете нарушение правила, но не видите его, обратитесь к Кодированию Стандартных Нарушений, Не Отображенных.
Группа: указатели и массивы |
Категория: необходимый |
Категория AGC: необходимый |