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