Этот пример показывает, как интерпретировать результаты Polyspace® Code Prover™, которые подсвечивают ошибку времени выполнения в цикле.
Если ошибка происходит в цикле, ошибка показывает в результатах анализа, когда красный Non-terminating loop проверяет ключевое слово цикла (for, while, и так далее).
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 только с небольшим количеством итераций.