Exponenta Banner

Non-terminating loop

Цикл не завершается или содержит ошибку

развернуть все на странице

Описание

Эта проверка цикла определяет, имеет ли цикл одну из следующих проблем:

  • Цикл определенно не завершается.

    Проверка появляется только в том случае, если Polyspace® не удается обнаружить выходной путь из цикла. Например, если цикл появляется в функции, и условие завершения цикла удовлетворяется для некоторых входных параметров функции, проверка не появляется, даже если условие может не выполняться для некоторых других входов.

  • Цикл содержит определенную ошибку в одной итерации.

    Несмотря на то, что определенная ошибка возникает в итерации одного цикла, поскольку верификация приводит к тому, что тело цикла агрегируется по всем итерациям цикла, ошибка показывает оранжевую проверку в теле цикла. Чтобы указать, что произошел определенный отказ, в команде loop отображается проверка Non-terminating loop красного цвета.

В отличие от других проверок, эта проверка появляется только тогда, когда возникает определенная ошибка. В результатах верификации чек всегда красный. Если ошибка возникает только в некоторых случаях, например, если привязка цикла переменна и вызывает проблему только для некоторых значений, проверка не отображается. Вместо этого команда loop отображается штриховым красным цветом с дополнительной информацией в подсказке.

Проверка также не отображается, если оба условия верны:

  • Цикл имеет тривиальный предикат, такой как for(;;) или while(1).

  • Цикл имеет пустое тело или тело без оператора выхода, такого как break, goto, return или исключение.

Вместо этого оператор цикла подчеркивается красными штрихами. Если вы поместите курсор в оператор цикла, то увидите, что верификация рассматривает цикл как преднамеренный. Если вы намеренно вводите бесконечные циклы, например, для эмуляции циклических задач, вы не должны обосновывать красные проверки.

Используя эту проверку, можно идентифицировать операцию в цикле, которая вызывает ошибку времени выполнения.

  • Чтобы найти источник ошибки, на панели Source установите курсор на вызове функции и просмотрите подсказку.

  • Для циклов с меньшим количеством итераций можно перейти к источнику ошибки в теле цикла. Выберите цикл, чтобы увидеть полную историю результата. Кроме того, щелкните правой кнопкой мыши ключевое слово цикла и выберите Go to Cause, если опция существует.

Примеры

расширить все

#include<stdio.h>

void main() {
  int i=0;
  while(i<10) {
    printf("%d",i);
  }
}

В этом примере, в while цикл, i не увеличивается. Поэтому тест i<10 никогда не прекращает работать.

Коррекция - обеспечьте разрыв цикла

Одной из возможных коррекций является обновление i таким образом, чтобы тест i<10 завершается неудачно после некоторых итераций цикла и цикла.

#include<stdio.h>

void main() {
  int i=0;
  while(i < 10) {
    printf("%d",i);
    i++;
  }
}
void main() {
  int arr[20];
  for(int i=0; i<=20; i++) {
    arr[i]=0;
  }
}

В этом примере последний запуск for цикл содержит Out of bounds array index ошибку. Поэтому Non-terminating loop проверяйте for цикл красный. Всплывающая подсказка появляется на for цикл с указанием максимального количества итераций, включая итерацию, содержащую ошибку времени выполнения.

Коррекция - Избегайте итерации цикла, содержащей ошибку

Одна возможная коррекция состоит в том, чтобы уменьшить количество итераций цикла, чтобы Out of bounds array index ошибка не произошла.

void main() {
  int arr[20];
  for(int i=0; i<20; i++) {
    arr[i]=0;
  }
}
int arr[4];

void assignValue(int index) {
  arr[index] = 0;
}

void main() {
  for(int i=0;i<=4;i++)
    assignValue(i);
}

В этом примере вызов функции assignValue в последней for итерация цикла содержит ошибку. Поэтому, хотя ошибка не показывает в for тело цикла, красный Non-terminating loop появляется на самом цикле.

Коррекция - Избегайте итерации цикла, содержащей ошибку

Одна из возможных коррекций состоит в том, чтобы уменьшить количество итераций цикла, чтобы ошибка в вызове assignValue не происходит.

int arr[4];

void assignValue(int index) {
  arr[index] = 0;
}

void main() {
 for(int i=0;i<4;i++)
   assignValue(i);
}
#define MAX 1024
void main() {
 int i=0,val=1;
 while(i<MAX) {
   val*=2;
   i++;
  }
}

В этом примере Overflow ошибка происходит в итерации № 31. Поэтому Non-terminating loop проверяйте while цикл красный. Всплывающая подсказка появляется на while цикл с указанием максимального количества итераций, включая итерацию, содержащую ошибку времени выполнения.

Коррекция - Уменьшайте итерации цикла

Одна возможная коррекция состоит в том, чтобы уменьшить количество итераций цикла, чтобы переполнение не произошло.

#define MAX 30
void main() {
 int i=0,val=1;
 while(i<MAX) {
   val*=2;
   i++;
  }
}

Проверяйте информацию

Группа: Управляйте потоком
Язык: C | C++
Акроним: NTL

См. также

Темы

Документация Polyspace Code Prover

Поддержка