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