Проблема возникает, когда счетчик цикла имеет плавающий тип.

Если на for индекс является символом переменной, Polyspace^® проверяет, что он не является плавающим.

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

Даже если цикл с счетчиком цикла с плавающей точкой ведет себя правильно в одной реализации, он может дать другое количество итерации в другой реализации.

int main(void){
    unsigned int counter = 0u;
    int result = 0;
    float foo;

    // Float loop counters
    for(float foo = 0.0f; foo < 1.0f; foo +=0.001f){ /*Non-compliant*/
        /*counter = 1000 at the end of the loop */
        ++counter;
    }

    float fff = 0.0f; 
    for(fff = 0.0f; fff <12.0f; fff += 1.0f){    /* Non-compliant*/
        result++;
    }

    // Integer loop count
    for(unsigned int count = 0u; count < 1000u; ++count){ /* Compliant */
        foo = (float) count * 0.001f;
    }
}

В этом примере три for циклы показывают три разных счетчика циклов. Первый и второй for циклы используют переменные с плавающей точкой в качестве счетчиков циклов, и поэтому не совместимы. В третьем цикле используется целое число count как счетчик цикла. Хотя count используется как значение с плавающей точкой внутри цикла, переменная остается целым числом при действии в качестве индекса цикла. Поэтому это for цикл совместим.

int main(void){
    unsigned int u32a;
    float foo;

    foo = 0.0f;
    while (foo < 1.0f){/* Non-compliant - foo used as a loop counter */
        foo += 0.001f;  
    }

    foo = read_float32();
    do{
        u32a = read_u32();
    }while( ((float)u32a - foo) > 10.0f );/* Compliant -  */
/*  foo doesn't change in the loop, so cannot be a counter */   
                        
    return 1; 
}

Этот пример показывает два while циклы, обе из которых используют foo в while-жаберные условия.

Первый while цикл использует foo в состоянии и внутри цикла. Потому что foo изменения, ошибки округления с плавающей точкой могут вызвать неожиданное поведение.

Вторая while цикл не использует foo внутри цикла, но использует foo внутри whileСостояние. Итак foo не является счетчиком цикла. Целое число u32a - счетчик цикла, поскольку он изменяется внутри цикла и является частью условия while. Потому что u32a является целым числом, проблема ошибки округления не является проблемой, делая это while совместимый с циклом.