Exponenta Banner

Non-terminating loop

Цикл не отключает или содержит ошибку

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

Описание

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

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

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

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

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

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

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

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

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

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

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

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

  • Циклы for с меньшим количеством итераций, можно перейти к источнику ошибки в теле цикла. Выберите цикл, чтобы видеть полную историю результата. В качестве альтернативы щелкните правой кнопкой по ключевому слову цикла и выберите 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

Поддержка