Exponenta Banner

Незавершение цикла

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

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

Описание

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

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

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

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

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

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

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

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

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

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

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

  • Чтобы найти источник ошибки, на панели 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
Поддержка