Удалите предположение по умолчанию о том, что внешние массивы неопределенного размера могут быть безопасно доступны при любом индексе
-consider-external-array-access-unsafe
-consider-external-array-access-unsafe удаляет используемое по умолчанию предположение о том, что доступ к внешним массивам неопределенного размера возможен при любом индексе. По умолчанию из-за этого предположения программа Code Prover показывает зеленый цвет Проверки индекса массива за пределами границ для внешнего массива обращается к коду, несмотря на то, что их размер неизвестен. При использовании этой опции та же проверка имеет оранжевый цвет и указывает на то, что доступ не является безопасным и требует проверки вручную.
Если анализ выполняется из пользовательского интерфейса (только для настольных продуктов Polyspace ®), на панели Конфигурация (Configuration) можно ввести этот параметр в поле Другое (Other). ПосмотритеOther.
Запустите программу проверки кода в этом примере с параметром и без него.
extern int arr[];
int getFifthElement(void) {
return arr[5];
}Доступ к массиву показывает зеленую проверку индекса массива вне границ без опции, но оранжевую проверку с опцией.