Удалите предположение по умолчанию, что к внешним массивам незаданного размера можно безопасно получить доступ в любом индексе
-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 без опции, но оранжевую проверку с опцией.