Этот пример показывает, как интерпретировать результаты Polyspace® Code Prover™, которые подсвечивают ошибку времени выполнения в цикле.
Если ошибка происходит в цикле, ошибка показывает в результатах анализа, когда красный Non-terminating loop проверяет ключевое слово цикла (forв то время как, и так далее).
for (i = 0; i <= 10; i++) В этом примере функция вызвана в цикле. Тело функции содержит другой цикл, который начинает операцию, вызывающую ошибку времени выполнения. Вы прослеживаете от первого цикла до операции, вызывающей ошибку времени выполнения.
Запустите верификацию на этом коде и откройте результаты:
int a[100];
int f (int i);
void main() {
int i,x=0;
for (i = 0; i <= 10; i++) {
x += f(i);
}
}
int f (int i) {
int j, x;
x = 0;
for (j = 0; j <= 10; j++) {
x += a[10 + (i * j)];
}
return x;
}Выберите красный результат Non-terminating loop. Панель Source подсвечивает for цикл в main.
Проследите от for цикл в main к операции, вызывающей ошибку. Операцией является x+= a[10 + (i*j)]. Ошибка Out of bounds array index происходит когда i 9 и j 10. Ошибка отображает оранжевым на [ оператор.
Прослеживать от красного for ключевое слово к оранжевой операции доступа к массиву:
Перейдите непосредственно к операции. Щелкните правой кнопкой по for ключевое слово и выбирает Go to Cause.
См. полную историю от for ключевое слово к операции доступа к массиву. Выберите красный for ключевое слово. Панель Result Details показывает историю.
Можно считать историю события в последовательности. Цикл внешнего цикла запускается девять раз без ошибки. На десятой итерации (i=9), цикл вводит функциональный f. В f, внутренний цикл запускается десять раз без ошибки. На одиннадцатой итерации (j=10), доступ к массиву вызывает ошибку.
Можно использовать эту информацию, чтобы определить, как закрепить ошибку времени выполнения на операции доступа к массиву.
Можно переместиться непосредственно к первопричине ошибки по циклам for только с небольшим количеством итераций.