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