В этом учебном пособии показано, как интерпретировать результаты Prover™ кода Polyspace ®, которые выделяют ошибку времени выполнения в цикле.
Если ошибка возникает в цикле, ошибка отображается в результатах анализа как красная проверка цикла без завершения по ключевому слову цикла (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. Панель «Источник» выделяет for цикл в main.
Трассировка из for цикл в main операции, вызывающей ошибку. Операция: x+= a[10 + (i*j)]. Ошибка индекса массива Out of bounds при i равно 9 и j составляет 10. Ошибка отображается оранжевым цветом на [ оператор.
Трассировка из красного цвета for ключевое слово операции доступа к оранжевому массиву:
Перейдите непосредственно к операции. Щелкните правой кнопкой мыши for и выберите Перейти к причине.
Просмотр полной истории из for ключевое слово операции доступа к массиву. Выберите красный цвет for ключевое слово. На панели Сведения о результате (Result Details) отображается история.
Историю событий можно прочитать последовательно. Внешний контур работает девять раз без ошибок. На десятой итерации (i=9), цикл входит в функцию f. Внутри fвнутренний цикл выполняется десять раз без ошибок. На одиннадцатой итерации (j=10), доступ к массиву приводит к ошибке.
Эту информацию можно использовать для определения способа исправления ошибки времени выполнения операции доступа к массиву.
Примечание
Можно перейти непосредственно к основной причине ошибки для циклов с небольшим количеством итераций.