В этом руководстве показано, как интерпретировать 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), доступ к массиву вызывает ошибку.
Можно использовать эту информацию, чтобы определить, как исправить ошибку времени выполнения операции доступа к массиву.
Примечание
Вы можете перейти непосредственно к первопричине ошибки для циклов с небольшим количеством итераций.