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