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

Если for index является символом переменной, 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 циклы используют переменные float в качестве счетчиков циклов и, следовательно, несовместимы. В третьем цикле используется целое число count в качестве счетчика циклов. Несмотря на то, что count используется в качестве float внутри цикла, переменная остается целым числом при работе в качестве индекса цикла. Поэтому это 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 совместимость с контуром.